set T = [:T1,T2:];
per cases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
suppose ( T1 is empty or T2 is empty ) ; :: thesis: [:T1,T2:] is T_2
hence [:T1,T2:] is T_2 ; :: thesis: verum
end;
suppose ( not T1 is empty & not T2 is empty ) ; :: thesis: [:T1,T2:] is T_2
then A1: not the carrier of [:T1,T2:] is empty ;
let p, q be Point of [:T1,T2:]; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )

assume A2: p <> q ; :: thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )

q in the carrier of [:T1,T2:] by A1;
then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider z, v being object such that
A3: z in the carrier of T1 and
A4: v in the carrier of T2 and
A5: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of [:T1,T2:] by A1;
then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider x, y being object such that
A6: x in the carrier of T1 and
A7: y in the carrier of T2 and
A8: p = [x,y] by ZFMISC_1:def 2;
reconsider y = y, v = v as Point of T2 by A7, A4;
reconsider x = x, z = z as Point of T1 by A6, A3;
per cases ( x <> z or x = z ) ;
suppose x <> z ; :: thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )

then consider Y, V being Subset of T1 such that
A9: ( Y is open & V is open ) and
A10: ( x in Y & z in V ) and
A11: Y misses V by PRE_TOPC:def 10;
reconsider Y = Y, V = V as Subset of T1 ;
reconsider X = [:Y,([#] T2):], Z = [:V,([#] T2):] as Subset of [:T1,T2:] ;
A12: X misses Z by ;
A13: ( X is open & Z is open ) by ;
( p in X & q in Z ) by ;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by ; :: thesis: verum
end;
suppose x = z ; :: thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )

then consider Y, V being Subset of T2 such that
A14: ( Y is open & V is open ) and
A15: ( y in Y & v in V ) and
A16: Y misses V by ;
reconsider Y = Y, V = V as Subset of T2 ;
reconsider X = [:([#] T1),Y:], Z = [:([#] T1),V:] as Subset of [:T1,T2:] ;
A17: X misses Z by ;
A18: ( X is open & Z is open ) by ;
( p in X & q in Z ) by ;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by ; :: thesis: verum
end;
end;
end;
end;