thus ( A is T_0 implies for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ) :: thesis:

proof

assume A1: A is T_0 ; :: thesis:
let a, b be Point of X; :: thesis:
assume that
A2: a in A and
A3: b in A ; :: thesis:
assume A4: a <> b ; :: thesis:

now :: thesis:

per cases by A1, A2, A3, A4, TSP_1:def 8;

suppose ex V being Subset of X st
( V is open & a in V & not b in V ) ; :: thesis:

then consider V being Subset of X such that
A5: V is open and
A6: a in V and
A7: not b in V ;

now :: thesis:

take V = V; :: thesis:
thus V is open by A5; :: thesis:
thus MaxADSet a c= V by A5, A6, TEX_4:24; :: thesis:
b in ([#] X) \ V by A7, XBOOLE_0:def 5;
then MaxADSet b c= V ` by A5, TEX_4:23;
hence V misses MaxADSet b by SUBSET_1:23; :: thesis:

end;

hence ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; :: thesis:

end;

suppose ex W being Subset of X st
( W is open & not a in W & b in W ) ; :: thesis:

then consider W being Subset of X such that
A8: W is open and
A9: not a in W and
A10: b in W ;

now :: thesis:

take W = W; :: thesis:
thus W is open by A8; :: thesis:
a in ([#] X) \ W by A9, XBOOLE_0:def 5;
then MaxADSet a c= W ` by A8, TEX_4:23;
hence W misses MaxADSet a by SUBSET_1:23; :: thesis:
thus MaxADSet b c= W by A8, A10, TEX_4:24; :: thesis:

end;

hence ( ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; :: thesis:

end;

end;

end;

hence MaxADSet a misses MaxADSet b by TEX_4:53; :: thesis:

end;

assume A11: for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ; :: thesis:

now :: thesis:

let a, b be Point of X; :: thesis:
assume that
A12: a in A and
A13: b in A ; :: thesis:
assume a <> b ; :: thesis:
then A14: MaxADSet a misses MaxADSet b by A11, A12, A13;

now :: thesis:

per cases by A14, TEX_4:53;

suppose ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) ; :: thesis:

then consider V being Subset of X such that
A15: V is open and
A16: MaxADSet a c= V and
A17: V misses MaxADSet b ;

now :: thesis:

take V = V; :: thesis:
thus V is open by A15; :: thesis:
{a} c= MaxADSet a by TEX_4:18;
then a in MaxADSet a by ZFMISC_1:31;
hence a in V by A16; :: thesis:

now :: thesis:

{b} c= MaxADSet b by TEX_4:18;
then A18: b in MaxADSet b by ZFMISC_1:31;
assume b in V ; :: thesis:
hence contradiction by A17, A18, XBOOLE_0:3; :: thesis:

end;

hence not b in V ; :: thesis:

end;

hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; :: thesis:

end;

suppose ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ; :: thesis:

then consider W being Subset of X such that
A19: W is open and
A20: W misses MaxADSet a and
A21: MaxADSet b c= W ;

now :: thesis:

take W = W; :: thesis:
thus W is open by A19; :: thesis:

now :: thesis:

{a} c= MaxADSet a by TEX_4:18;
then A22: a in MaxADSet a by ZFMISC_1:31;
assume a in W ; :: thesis:
hence contradiction by A20, A22, XBOOLE_0:3; :: thesis:

end;

hence not a in W ; :: thesis:
{b} c= MaxADSet b by TEX_4:18;
then b in MaxADSet b by ZFMISC_1:31;
hence b in W by A21; :: thesis:

end;

hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; :: thesis:

end;

end;

end;

hence ( ex V being Subset of X st
( V is open & a in V & not b in V ) or ex W being Subset of X st
( W is open & not a in W & b in W ) ) ; :: thesis:

end;

hence A is T_0 by TSP_1:def 8; :: thesis: