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 ‘ ≤ )