let a, b, r, s be Real; ( 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 )
; 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; verum