set T = [:T1,T2:];

per cases
( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) )
;

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 b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} ) )

assume A2: p <> q ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

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;

end;let p, q be Point of [:T1,T2:]; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b

( b

assume A2: p <> q ; :: thesis: ex b

( b

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 )
;

end;

suppose
x <> z
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

( b

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 A11, ZFMISC_1:104;

A13: ( X is open & Z is open ) by A9, BORSUK_1:6;

( p in X & q in Z ) by A7, A8, A4, A5, A10, ZFMISC_1:87;

hence ex b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )
by A13, A12; :: thesis: verum

end;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 A11, ZFMISC_1:104;

A13: ( X is open & Z is open ) by A9, BORSUK_1:6;

( p in X & q in Z ) by A7, A8, A4, A5, A10, ZFMISC_1:87;

hence ex b

( b

suppose
x = z
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

( b

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 A2, A8, A5, PRE_TOPC:def 10;

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 A16, ZFMISC_1:104;

A18: ( X is open & Z is open ) by A14, BORSUK_1:6;

( p in X & q in Z ) by A6, A8, A3, A5, A15, ZFMISC_1:87;

hence ex b_{1}, b_{2} being Element of bool the carrier of [:T1,T2:] st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )
by A18, A17; :: thesis: verum

end;A14: ( Y is open & V is open ) and

A15: ( y in Y & v in V ) and

A16: Y misses V by A2, A8, A5, PRE_TOPC:def 10;

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 A16, ZFMISC_1:104;

A18: ( X is open & Z is open ) by A14, BORSUK_1:6;

( p in X & q in Z ) by A6, A8, A3, A5, A15, ZFMISC_1:87;

hence ex b

( b