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:

proof

assume A1: A is anti-discrete ; :: thesis:
let x, y be Point of X; :: thesis:
assume that
A2: x in A and
A3: y in A ; :: thesis:
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:

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:

proof

assume A5: for x, y being Point of X st x in A & y in A holds
Cl {x} = Cl {y} ; :: thesis:

now :: thesis:

let x be Point of X; :: thesis:
assume A6: x in A ; :: thesis:

now :: thesis:

let a be object ; :: thesis:
assume A7: a in A ; :: thesis:
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:

end;

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

end;

hence A is anti-discrete ; :: thesis:

end;