thus ( A is T_0 implies for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) :: thesis: ( ( for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) implies A is T_0 )

proof

assume A1: A is T_0 ; :: thesis: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a}
let a be Point of X; :: thesis: ( a in A implies A /\ (MaxADSet a) = {a} )
{a} c= MaxADSet a by TEX_4:20;
then A2: a in MaxADSet a by ZFMISC_1:37;
assume A3: a in A ; :: thesis: A /\ (MaxADSet a) = {a}
then A4: a in A /\ (MaxADSet a) by A2, XBOOLE_0:def 4;
assume A /\ (MaxADSet a) <> {a} ; :: thesis: contradiction
then consider b being set such that
A5: b in A /\ (MaxADSet a) and
A6: b <> a by A4, ZFMISC_1:41;
reconsider b = b as Point of X by A5;
b in A by A5, XBOOLE_0:def 4;
then A7: MaxADSet a misses MaxADSet b by A1, A3, A6, Def1;
b in MaxADSet a by A5, XBOOLE_0:def 4;
hence contradiction by A7, TEX_4:23; :: thesis: verum

end;

assume A8: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ; :: thesis: A is T_0

now

let a, b be Point of X; :: thesis: ( a in A & b in A & a <> b implies not MaxADSet a meets MaxADSet b )
assume ( a in A & b in A ) ; :: thesis: ( a <> b implies not MaxADSet a meets MaxADSet b )
then A9: ( A /\ (MaxADSet a) = {a} & A /\ (MaxADSet b) = {b} ) by A8;
assume A10: a <> b ; :: thesis: not MaxADSet a meets MaxADSet b
assume MaxADSet a meets MaxADSet b ; :: thesis: contradiction
then {a} = {b} by A9, TEX_4:24;
hence contradiction by A10, ZFMISC_1:6; :: thesis: verum

end;

hence A is T_0 by Def1; :: thesis: verum