Metamath Proof Explorer


Theorem reordt

Description: The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion reordt ordTop

Proof

Step Hyp Ref Expression
1 ioomax −∞+∞=
2 iooordt −∞+∞ordTop
3 1 2 eqeltrri ordTop