let a, b, r, s be real number ; :: 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:25;
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 Th51;
then product (1,2 --> A,B) c= closed_inside_of_rectangle a,b,r,s by A1, TOPREAL6:29;
hence product (1,2 --> A,B) is Subset of (Trectangle a,b,r,s) by PRE_TOPC:29; :: thesis: verum