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 ` <_ ) |`t ( A [,] B ) ) = ( ordTop ` ( <_ i^i ( ( A [,] B ) X. ( A [,] B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccssxr	|- ( A [,] B ) C_ RR*
2		iccss2	|- ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( x [,] y ) C_ ( A [,] B ) )
3	1 2	ordtrestixx	|- ( ( ordTop ` <_ ) |`t ( A [,] B ) ) = ( ordTop ` ( <_ i^i ( ( A [,] B ) X. ( A [,] B ) ) ) )