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 A c= Cl {x} by A1, Def12;
then A3: Cl A c= Cl {x} by TOPS_1:31;
{x} c= A by A2, ZFMISC_1:37;
then Cl {x} c= Cl A by PRE_TOPC:49;
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} & A c= Cl A ) by A4, PRE_TOPC:48;
hence A c= Cl {x} ; :: thesis: verum

end;

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