let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies for A being closed Subset of (Closed-Interval-TSpace a,b)
for B being closed Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s) )
set T = Closed-Interval-TSpace a,b;
set S = Closed-Interval-TSpace r,s;
assume A1: ( a <= b & r <= s ) ; :: thesis: for A being closed Subset of (Closed-Interval-TSpace a,b)
for B being closed Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s)
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;
let A be closed Subset of (Closed-Interval-TSpace a,b); :: thesis: for B being closed Subset of (Closed-Interval-TSpace r,s) holds product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s)
let B be closed Subset of (Closed-Interval-TSpace r,s); :: thesis: product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s)
reconsider P = product (1,2 --> A,B) as Subset of (Trectangle a,b,r,s) by A1, Th60;
A2: [:A,B:] is closed by TOPALG_3:16;
the carrier of (Closed-Interval-TSpace r,s) is Subset of R^1 by TSEP_1:1;
then A3: B is Subset of REAL by TOPMETR:24, XBOOLE_1:1;
the carrier of (Closed-Interval-TSpace a,b) is Subset of R^1 by TSEP_1:1;
then A4: A is Subset of REAL by TOPMETR:24, XBOOLE_1:1;
A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:162
.= P by A4, A3, Th55 ;
( h is being_homeomorphism & not Trectangle a,b,r,s is empty ) by A1, Th54, Th58;
hence product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s) by A5, A2, TOPS_2:72; :: thesis: verum