let a, b, r, s be Real; :: 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:18;
hence the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] by BORSUK_1:def 2; :: thesis: verum