let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):], Trectangle a,b,r,s are_homeomorphic )
set C1 = Closed-Interval-TSpace a,b;
set C2 = Closed-Interval-TSpace r,s;
assume A1: ( a <= b & r <= s ) ; :: thesis: [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):], Trectangle a,b,r,s are_homeomorphic
then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] as Function of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):],(Trectangle a,b,r,s) by Th57;
take h ; :: according to T_0TOPSP:def 1 :: thesis: h is being_homeomorphism
thus h is being_homeomorphism by A1, Th58; :: thesis: verum