thus ( A is anti-discrete implies for x being Point of X st x in A holds
A c= Cl {x} ) :: thesis: ( ( for x being Point of X st x in A holds
A c= Cl {x} ) implies A is anti-discrete )

proof

assume A1: A is anti-discrete ; :: thesis: for x being Point of X st x in A holds
A c= Cl {x}
let x be Point of X; :: thesis: ( x in A implies A c= Cl {x} )
assume A2: x in A ; :: thesis: A c= Cl {x}
{x} c= Cl {x} by PRE_TOPC:18;
then A3: x in Cl {x} by ZFMISC_1:31;
( A misses Cl {x} or A c= Cl {x} ) by A1;
hence A c= Cl {x} by A2, A3, XBOOLE_0:3; :: thesis: verum

end;

thus ( ( for x being Point of X st x in A holds
A c= Cl {x} ) implies A is anti-discrete ) :: thesis: verum

proof

assume A4: for x being Point of X st x in A holds
A c= Cl {x} ; :: thesis: A is anti-discrete

now :: thesis: for F being Subset of X st F is closed & A meets F holds
A c= F

let F be Subset of X; :: thesis: ( F is closed & A meets F implies A c= F )
assume A5: F is closed ; :: thesis: ( A meets F implies A c= F )
assume A meets F ; :: thesis: A c= F
then consider a being object such that
A6: a in A /\ F by XBOOLE_0:4;
reconsider a = a as Point of X by A6;
a in F by A6, XBOOLE_0:def 4;
then {a} c= F by ZFMISC_1:31;
then A7: Cl {a} c= F by A5, TOPS_1:5;
a in A by A6, XBOOLE_0:def 4;
then A c= Cl {a} by A4;
hence A c= F by A7; :: thesis: verum

end;

hence A is anti-discrete ; :: thesis: verum

end;