let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies for A being Subset of
for B being Subset of holds product (1,2 --> A,B) is Subset of )
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
for B being Subset of holds product (1,2 --> A,B) is Subset of
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 ; :: thesis: for B being Subset of holds product (1,2 --> A,B) is Subset of
let B be Subset of ; :: thesis: product (1,2 --> A,B) is Subset of
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 by PRE_TOPC:29; :: thesis: verum