Theorem ordtresticc

Description: The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Assertion	ordtresticc	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[A,B\right]=\mathrm{ordTop}\left(\le \cap \left(\left[A,B\right]\times \left[A,B\right]\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		iccssxr	$$⊢\left[A,B\right]\subseteq {ℝ}^{*}$$
2		iccss2	$$⊢\left(x\in \left[A,B\right]\wedge y\in \left[A,B\right]\right)\to \left[x,y\right]\subseteq \left[A,B\right]$$
3	1 2	ordtrestixx	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[A,B\right]=\mathrm{ordTop}\left(\le \cap \left(\left[A,B\right]\times \left[A,B\right]\right)\right)$$