set T = [:T1,T2:];

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

end;

suppose that A1:
not T1 is empty
and

A2: not T2 is empty ; :: thesis: [:T1,T2:] is T_0

A2: not T2 is empty ; :: thesis: [:T1,T2:] is T_0

A3:
not the carrier of [:T1,T2:] is empty
by A1, A2;

end;now :: thesis: for p, q being Point of [:T1,T2:] st p <> q holds

ex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) )

hence
[:T1,T2:] is T_0
; :: thesis: verumex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) )

let p, q be Point of [:T1,T2:]; :: thesis: ( p <> q implies ex X being Subset of [:T1,T2:] st

( b_{3} is open & ( ( X in b_{3} & not b_{2} in b_{3} ) or ( b_{2} in b_{3} & not X in b_{3} ) ) ) )

assume A4: p <> q ; :: thesis: ex X being Subset of [:T1,T2:] st

( b_{3} is open & ( ( X in b_{3} & not b_{2} in b_{3} ) or ( b_{2} in b_{3} & not X in b_{3} ) ) )

q in the carrier of [:T1,T2:] by A3;

then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

then consider z, v being object such that

A5: z in the carrier of T1 and

A6: v in the carrier of T2 and

A7: q = [z,v] by ZFMISC_1:def 2;

p in the carrier of [:T1,T2:] by A3;

then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

then consider x, y being object such that

A8: x in the carrier of T1 and

A9: y in the carrier of T2 and

A10: p = [x,y] by ZFMISC_1:def 2;

reconsider y = y, v = v as Point of T2 by A9, A6;

reconsider x = x, z = z as Point of T1 by A8, A5;

end;( b

assume A4: p <> q ; :: thesis: ex X being Subset of [:T1,T2:] st

( b

q in the carrier of [:T1,T2:] by A3;

then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

then consider z, v being object such that

A5: z in the carrier of T1 and

A6: v in the carrier of T2 and

A7: q = [z,v] by ZFMISC_1:def 2;

p in the carrier of [:T1,T2:] by A3;

then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

then consider x, y being object such that

A8: x in the carrier of T1 and

A9: y in the carrier of T2 and

A10: p = [x,y] by ZFMISC_1:def 2;

reconsider y = y, v = v as Point of T2 by A9, A6;

reconsider x = x, z = z as Point of T1 by A8, A5;

per cases
( x <> z or x = z )
;

end;

suppose
x <> z
; :: thesis: ex X being Subset of [:T1,T2:] st

( b_{3} is open & ( ( X in b_{3} & not b_{2} in b_{3} ) or ( b_{2} in b_{3} & not X in b_{3} ) ) )

( b

then consider V1 being Subset of T1 such that

A11: V1 is open and

A12: ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A1, T_0TOPSP:def 7;

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

hence ex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A13; :: thesis: verum

end;A11: V1 is open and

A12: ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A1, T_0TOPSP:def 7;

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

A13: now :: thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )end;

[:V1,([#] T2):] is open
by A11, BORSUK_1:6;per cases
( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) )
by A12;

end;

suppose
( x in V1 & not z in V1 )
; :: thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )

hence
( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )
by A9, A10, A7, ZFMISC_1:87; :: thesis: verum

end;suppose
( z in V1 & not x in V1 )
; :: thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )

hence
( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )
by A10, A6, A7, ZFMISC_1:87; :: thesis: verum

end;hence ex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A13; :: thesis: verum

suppose
x = z
; :: thesis: ex X being Subset of [:T1,T2:] st

( b_{3} is open & ( ( X in b_{3} & not b_{2} in b_{3} ) or ( b_{2} in b_{3} & not X in b_{3} ) ) )

( b

then consider V1 being Subset of T2 such that

A14: V1 is open and

A15: ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A4, A10, A7, A2, T_0TOPSP:def 7;

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

hence ex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A16; :: thesis: verum

end;A14: V1 is open and

A15: ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A4, A10, A7, A2, T_0TOPSP:def 7;

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

A16: now :: thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )end;

[:([#] T1),V1:] is open
by A14, BORSUK_1:6;per cases
( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) )
by A15;

end;

suppose
( y in V1 & not v in V1 )
; :: thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )

hence
( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )
by A8, A10, A7, ZFMISC_1:87; :: thesis: verum

end;suppose
( v in V1 & not y in V1 )
; :: thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )

hence
( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )
by A10, A5, A7, ZFMISC_1:87; :: thesis: verum

end;hence ex X being Subset of [:T1,T2:] st

( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A16; :: thesis: verum