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 that
A2: x in A and
A3: y in A ; :: thesis: Cl {x} = Cl {y}
A c= Cl {y} by A1, A3;
then {x} c= Cl {y} by A2, ZFMISC_1:31;
then A4: Cl {x} c= Cl {y} by TOPS_1:5;
A c= Cl {x} by A1, A2;
then {y} c= Cl {x} by A3, ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
hence Cl {x} = Cl {y} by A4; :: 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 A5: 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 :: 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 A6: x in A ; :: thesis: A c= Cl {x}

now :: thesis: for a being object st a in A holds
a in Cl {x}

let a be object ; :: thesis: ( a in A implies a in Cl {x} )
assume A7: a in A ; :: thesis: a in Cl {x}
then reconsider y = a as Point of X ;
{y} c= Cl {y} by PRE_TOPC:18;
then y in Cl {y} by ZFMISC_1:31;
hence a in Cl {x} by A5, A6, A7; :: thesis: verum

end;

hence A c= Cl {x} ; :: thesis: verum

end;

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

end;