set T = [:T1,T2:];
per cases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
suppose ( T1 is empty or T2 is empty ) ; :: thesis: [:T1,T2:] is T_0
hence [:T1,T2:] is T_0 ; :: thesis: verum
end;
suppose that A1: not T1 is empty and
A2: not T2 is empty ; :: thesis: [:T1,T2:] is T_0
A3: not the carrier of [:T1,T2:] is empty by A1, A2;
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 ) ) )
let p, q be Point of [:T1,T2:]; :: thesis: ( p <> q implies ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) )
assume A4: p <> q ; :: thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
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 ) ;
suppose x <> z ; :: thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
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):];
A13: now :: thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )
per cases ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A12;
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;
end;
end;
[:V1,([#] T2):] is open by A11, BORSUK_1:6;
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;
suppose x = z ; :: thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
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:];
A16: now :: thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )
per cases ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A15;
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;
end;
end;
[:([#] T1),V1:] is open by A14, BORSUK_1:6;
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;
end;
end;
hence [:T1,T2:] is T_0 ; :: thesis: verum
end;
end;