let a, b, r, s be Real; :: thesis: ( a <= b & r <= s implies for A being open Subset of (Closed-Interval-TSpace (a,b))
for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open 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 open Subset of (Closed-Interval-TSpace (a,b))
for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open 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 Th35;
let A be open Subset of (Closed-Interval-TSpace (a,b)); :: thesis: for B being open Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
let B be open Subset of (Closed-Interval-TSpace (r,s)); :: thesis: product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s))
reconsider P = product ((1,2) --> (A,B)) as Subset of (Trectangle (a,b,r,s)) by A1, Th38;
A2: [:A,B:] is open by BORSUK_1:6;
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:17, 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:17, XBOOLE_1:1;
A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:129
.= P by A4, A3, Th33 ;
( h is being_homeomorphism & not Trectangle (a,b,r,s) is empty ) by A1, Th32, Th36;
hence product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s)) by A5, A2, TOPGRP_1:25; :: thesis: verum