set T = [:T1,T2:];

now

let p, q be Point of [:T1,T2:]; :: thesis: ( p <> q implies ex X being Subset of [:T1,T2:] st
( b₃ is open & ( ( X in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not X in b₃ ) ) ) )
assume A1: p <> q ; :: thesis: ex X being Subset of [:T1,T2:] st
( b₃ is open & ( ( X in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not X in b₃ ) ) )
q in the carrier of [:T1,T2:] ;
then q in [:the carrier of T1,the carrier of T2:] by BORSUK_1:def 5;
then consider z, v being set such that
A2: z in the carrier of T1 and
A3: v in the carrier of T2 and
A4: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of [:T1,T2:] ;
then p in [:the carrier of T1,the carrier of T2:] by BORSUK_1:def 5;
then consider x, y being set such that
A5: x in the carrier of T1 and
A6: y in the carrier of T2 and
A7: p = [x,y] by ZFMISC_1:def 2;
reconsider y = y, v = v as Point of T2 by A6, A3;
reconsider x = x, z = z as Point of T1 by A5, A2;

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

suppose x <> z ; :: thesis: ex X being Subset of [:T1,T2:] st
( b₃ is open & ( ( X in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not X in b₃ ) ) )

then consider V1 being Subset of T1 such that
A8: V1 is open and
A9: ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by T_0TOPSP:def 7;
set X = [:V1,([#] T2):];

A10: now

per cases ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A9;

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 A6, A7, A4, ZFMISC_1:106; :: 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 A7, A3, A4, ZFMISC_1:106; :: thesis: verum

end;

end;

end;

[#] T2 is open ;
then [:V1,([#] T2):] is open by A8, BORSUK_1:46;
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 A10; :: thesis: verum

end;

suppose x = z ; :: thesis: ex X being Subset of [:T1,T2:] st
( b₃ is open & ( ( X in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not X in b₃ ) ) )

then consider V1 being Subset of T2 such that
A11: V1 is open and
A12: ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A1, A7, A4, T_0TOPSP:def 7;
set X = [:([#] T1),V1:];

A13: now

per cases ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A12;

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 A5, A7, A4, ZFMISC_1:106; :: 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 A7, A2, A4, ZFMISC_1:106; :: thesis: verum

end;

end;

end;

[#] T1 is open ;
then [:([#] T1),V1:] is open by A11, BORSUK_1:46;
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;

end;

end;

hence [:T1,T2:] is T_0 by T_0TOPSP:def 7; :: thesis: verum