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 that
A1: a <= b and
A2: 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)
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, A2, Th60;
( the carrier of (Closed-Interval-TSpace a,b) is Subset of R^1 & the carrier of (Closed-Interval-TSpace r,s) is Subset of R^1 ) by TSEP_1:1;
then A3: ( A is Subset of REAL & B is Subset of REAL ) by TOPMETR:24, XBOOLE_1:1;
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 A1, A2, Th57;
A4: h is being_homeomorphism by A1, A2, Th58;
A5: not Trectangle a,b,r,s is empty by A1, A2, Th54;
A6: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:162
.= P by A3, Th55 ;
[:A,B:] is closed by TOPALG_3:16;
hence product (1,2 --> A,B) is closed Subset of (Trectangle a,b,r,s) by A4, A5, A6, TOPS_2:72; :: thesis: verum