let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:] )
set C1 = Closed-Interval-TSpace a,b;
set C2 = Closed-Interval-TSpace r,s;
assume ( a <= b & r <= s ) ; :: thesis: the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:]
then ( the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] & the carrier of (Closed-Interval-TSpace r,s) = [.r,s.] ) by TOPMETR:25;
hence the carrier of [:(Closed-Interval-TSpace a,b),(Closed-Interval-TSpace r,s):] = [:[.a,b.],[.r,s.]:] by BORSUK_1:def 5; :: thesis: verum