let a, b, r, s be Real; :: thesis: ( a <= b & r <= s implies for A being Subset of (Closed-Interval-TSpace (a,b))
for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) )
set T = Closed-Interval-TSpace (a,b);
set S = Closed-Interval-TSpace (r,s);
assume ( a <= b & r <= s ) ; :: thesis: for A being Subset of (Closed-Interval-TSpace (a,b))
for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
then A1: ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] ) by TOPMETR:18;
let A be Subset of (Closed-Interval-TSpace (a,b)); :: thesis: for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
let B be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s))
closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.])) by Th30;
then product ((1,2) --> (A,B)) c= closed_inside_of_rectangle (a,b,r,s) by A1, TOPREAL6:21;
hence product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) by PRE_TOPC:8; :: thesis: verum