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₃ ) ) )
( p in the carrier of [:T1,T2:] & q in the carrier of [:T1,T2:] ) ;
then A2: ( p in [:the carrier of T1,the carrier of T2:] & q in [:the carrier of T1,the carrier of T2:] ) by BORSUK_1:def 5;
then consider x, y being set such that
A3: ( x in the carrier of T1 & y in the carrier of T2 & p = [x,y] ) by ZFMISC_1:def 2;
consider z, v being set such that
A4: ( z in the carrier of T1 & v in the carrier of T2 & q = [z,v] ) by A2, ZFMISC_1:def 2;
reconsider x = x, z = z as Point of T1 by A3, A4;
reconsider y = y, v = v as Point of T2 by A3, A4;

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
A5: ( V1 is open & ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) ) by T_0TOPSP:def 7;
A6: [#] T2 is open by TOPS_1:53;
set X = [:V1,([#] T2):];
A7: [:V1,([#] T2):] is open by A5, A6, BORSUK_1:46;

now

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

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

end;

end;

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 A7; :: 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
A8: ( V1 is open & ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) ) by A1, A3, A4, T_0TOPSP:def 7;
A9: [#] T1 is open by TOPS_1:53;
set X = [:([#] T1),V1:];
A10: [:([#] T1),V1:] is open by A8, A9, BORSUK_1:46;

now

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

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

end;

end;

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 A10; :: thesis: verum

end;

end;

end;

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