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

proof

assume A1: A is anti-discrete ; :: thesis: for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y}
let x, y be Point of X; :: thesis: ( x in A & y in A implies Cl {x} = Cl {y} )
assume A2: ( x in A & y in A ) ; :: thesis: Cl {x} = Cl {y}
then ( A c= Cl {x} & A c= Cl {y} ) by A1, Def12;
then ( {y} c= Cl {x} & {x} c= Cl {y} ) by A2, ZFMISC_1:37;
then ( Cl {y} c= Cl {x} & Cl {x} c= Cl {y} ) by TOPS_1:31;
hence Cl {x} = Cl {y} by XBOOLE_0:def 10; :: thesis: verum

end;

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

proof

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

now

let x be Point of X; :: thesis: ( x in A implies A c= Cl {x} )
assume A4: x in A ; :: thesis: A c= Cl {x}

now

let a be set ; :: thesis: ( a in A implies a in Cl {x} )
assume A5: a in A ; :: thesis: a in Cl {x}
then reconsider y = a as Point of X ;
{y} c= Cl {y} by PRE_TOPC:48;
then y in Cl {y} by ZFMISC_1:37;
hence a in Cl {x} by A3, A4, A5; :: thesis: verum

end;

hence A c= Cl {x} by TARSKI:def 3; :: thesis: verum

end;

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

end;