thus ( A is anti-discrete implies for x being Point of X st x in A holds
Cl A = Cl {x} ) :: thesis: ( ( for x being Point of X st x in A holds
Cl A = 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
Cl A = Cl {x}
let x be Point of X; :: thesis: ( x in A implies Cl A = Cl {x} )
assume A2: x in A ; :: thesis: Cl A = Cl {x}
then {x} c= A by ZFMISC_1:31;
then A3: Cl {x} c= Cl A by PRE_TOPC:19;
A c= Cl {x} by A1, A2, Def12;
then Cl A c= Cl {x} by TOPS_1:5;
hence Cl A = Cl {x} by A3, XBOOLE_0:def 10; :: thesis: verum

end;

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

now

let x be Point of X; :: thesis: ( x in A implies A c= Cl {x} )
assume x in A ; :: thesis: A c= Cl {x}
then Cl A = Cl {x} by A4;
hence A c= Cl {x} by PRE_TOPC:18; :: thesis: verum

end;

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