Metamath Proof Explorer


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 ordTop 𝑡 A B = ordTop A B × A B

Proof

Step Hyp Ref Expression
1 iccssxr A B *
2 iccss2 x A B y A B x y A B
3 1 2 ordtrestixx ordTop 𝑡 A B = ordTop A B × A B