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: ( ( for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b ) implies A is T_0 )

proof

assume A1: A is T_0 ; :: thesis: for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b
let a, b be Point of X; :: thesis: ( a in A & b in A & a <> b implies MaxADSet a misses MaxADSet b )
assume A2: ( a in A & b in A ) ; :: thesis: ( not a <> b or MaxADSet a misses MaxADSet b )
assume A3: a <> b ; :: thesis: MaxADSet a misses MaxADSet b

now

per cases ( 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 ) ) by A1, A2, A3, TSP_1:def 8;

suppose ex V being Subset of X st
( V is open & a in V & not b in V ) ; :: thesis: ( 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 ) )

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

now

take V = V; :: thesis: ( V is open & MaxADSet a c= V & V misses MaxADSet b )
thus V is open by A4; :: thesis: ( MaxADSet a c= V & V misses MaxADSet b )
thus MaxADSet a c= V by A4, A5, TEX_4:26; :: thesis: V misses MaxADSet b
( V = ([#] X) \ (([#] X) \ V) & b in [#] X ) by PRE_TOPC:22;
then ( ([#] X) \ V is closed & b in ([#] X) \ V ) by A4, A6, PRE_TOPC:def 6, XBOOLE_0:def 5;
then MaxADSet b c= V ` by TEX_4:25;
hence V misses MaxADSet b by SUBSET_1:43; :: thesis: verum

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: verum

end;

suppose ex W being Subset of X st
( W is open & not a in W & b in W ) ; :: thesis: ( 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 ) )

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

now

take W = W; :: thesis: ( W is open & W misses MaxADSet a & MaxADSet b c= W )
thus W is open by A7; :: thesis: ( W misses MaxADSet a & MaxADSet b c= W )
( W = ([#] X) \ (([#] X) \ W) & a in [#] X ) by PRE_TOPC:22;
then ( ([#] X) \ W is closed & a in ([#] X) \ W ) by A7, A8, PRE_TOPC:def 6, XBOOLE_0:def 5;
then MaxADSet a c= W ` by TEX_4:25;
hence W misses MaxADSet a by SUBSET_1:43; :: thesis: MaxADSet b c= W
thus MaxADSet b c= W by A7, A9, TEX_4:26; :: thesis: verum

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: verum

end;

end;

end;

hence MaxADSet a misses MaxADSet b by TEX_4:55; :: thesis: verum

end;

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

now

let a, b be Point of X; :: thesis: ( a in A & b in A & a <> b & ( for V being Subset of X holds
( not V is open or not a in V or b in V ) ) implies ex W being Subset of X st
( W is open & not a in W & b in W ) )
assume A11: ( a in A & b in A ) ; :: thesis: ( not a <> b or 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 ) )
assume a <> b ; :: thesis: ( 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 ) )
then A12: MaxADSet a misses MaxADSet b by A10, A11;

now

per cases ( 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 ) ) by A12, TEX_4:55;

suppose ex V being Subset of X st
( V is open & MaxADSet a c= V & V misses MaxADSet b ) ; :: thesis: ( 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 ) )

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

now

take V = V; :: thesis: ( V is open & a in V & not b in V )
thus V is open by A13; :: thesis: ( a in V & not b in V )
{a} c= MaxADSet a by TEX_4:20;
then a in MaxADSet a by ZFMISC_1:37;
hence a in V by A14; :: thesis: not b in V

now

assume A16: b in V ; :: thesis: contradiction
{b} c= MaxADSet b by TEX_4:20;
then b in MaxADSet b by ZFMISC_1:37;
hence contradiction by A15, A16, XBOOLE_0:3; :: thesis: verum

end;

hence not b in V ; :: thesis: verum

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: verum

end;

suppose ex W being Subset of X st
( W is open & W misses MaxADSet a & MaxADSet b c= W ) ; :: thesis: ( 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 ) )

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

now

take W = W; :: thesis: ( W is open & not a in W & b in W )
thus W is open by A17; :: thesis: ( not a in W & b in W )

now

assume A20: a in W ; :: thesis: contradiction
{a} c= MaxADSet a by TEX_4:20;
then a in MaxADSet a by ZFMISC_1:37;
hence contradiction by A18, A20, XBOOLE_0:3; :: thesis: verum

end;

hence not a in W ; :: thesis: b in W
{b} c= MaxADSet b by TEX_4:20;
then b in MaxADSet b by ZFMISC_1:37;
hence b in W by A19; :: thesis: verum

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: verum

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: verum

end;

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