let a, b, r, s be Real; :: 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 Th35;
take h ; :: according to T_0TOPSP:def 1 :: thesis: h is being_homeomorphism
thus h is being_homeomorphism by A1, Th36; :: thesis: verum