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	$$⊢ℝ\in \mathrm{ordTop}\left(\le \right)$$

Proof

Step	Hyp	Ref	Expression
1		ioomax	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$$
2		iooordt	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)\in \mathrm{ordTop}\left(\le \right)$$
3	1 2	eqeltrri	$$⊢ℝ\in \mathrm{ordTop}\left(\le \right)$$