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_1

then A1:
not the carrier of [:T1,T2:] is empty
;

let p, q be Point of [:T1,T2:]; :: according to URYSOHN1:def 7 :: 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} & not q in b_{1} & q in b_{2} & not p in 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} & not q in b_{1} & q in b_{2} & not p in 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 URYSOHN1:def 7 :: 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} & not q in b_{1} & q in b_{2} & not p in 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 and

A11: not z in Y and

A12: z in V and

A13: not x in V by URYSOHN1:def 7;

set X = [:Y,([#] T2):];

set Z = [:V,([#] T2):];

A14: ( not q in [:Y,([#] T2):] & not p in [:V,([#] T2):] ) by A8, A5, A11, A13, ZFMISC_1:87;

A15: ( [:Y,([#] T2):] is open & [:V,([#] T2):] is open ) by A9, BORSUK_1:6;

( p in [:Y,([#] T2):] & q in [:V,([#] T2):] ) by A7, A8, A4, A5, A10, A12, 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} & not q in b_{1} & q in b_{2} & not p in b_{2} )
by A15, A14; :: thesis: verum

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

A10: x in Y and

A11: not z in Y and

A12: z in V and

A13: not x in V by URYSOHN1:def 7;

set X = [:Y,([#] T2):];

set Z = [:V,([#] T2):];

A14: ( not q in [:Y,([#] T2):] & not p in [:V,([#] T2):] ) by A8, A5, A11, A13, ZFMISC_1:87;

A15: ( [:Y,([#] T2):] is open & [:V,([#] T2):] is open ) by A9, BORSUK_1:6;

( p in [:Y,([#] T2):] & q in [:V,([#] T2):] ) by A7, A8, A4, A5, A10, A12, 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} & not q in b_{1} & q in b_{2} & not p in b_{2} )

( b

then consider Y, V being Subset of T2 such that

A16: ( Y is open & V is open ) and

A17: y in Y and

A18: not v in Y and

A19: v in V and

A20: not y in V by A2, A8, A5, URYSOHN1:def 7;

reconsider Y = Y, V = V as Subset of T2 ;

set X = [:([#] T1),Y:];

set Z = [:([#] T1),V:];

A21: ( not p in [:([#] T1),V:] & not q in [:([#] T1),Y:] ) by A8, A5, A18, A20, ZFMISC_1:87;

A22: ( [:([#] T1),Y:] is open & [:([#] T1),V:] is open ) by A16, BORSUK_1:6;

( p in [:([#] T1),Y:] & q in [:([#] T1),V:] ) by A6, A8, A3, A5, A17, A19, 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} & not q in b_{1} & q in b_{2} & not p in b_{2} )
by A22, A21; :: thesis: verum

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

A17: y in Y and

A18: not v in Y and

A19: v in V and

A20: not y in V by A2, A8, A5, URYSOHN1:def 7;

reconsider Y = Y, V = V as Subset of T2 ;

set X = [:([#] T1),Y:];

set Z = [:([#] T1),V:];

A21: ( not p in [:([#] T1),V:] & not q in [:([#] T1),Y:] ) by A8, A5, A18, A20, ZFMISC_1:87;

A22: ( [:([#] T1),Y:] is open & [:([#] T1),V:] is open ) by A16, BORSUK_1:6;

( p in [:([#] T1),Y:] & q in [:([#] T1),V:] ) by A6, A8, A3, A5, A17, A19, ZFMISC_1:87;

hence ex b

( b