thus
( A is anti-discrete implies for x being Point of X st x in A holds

Cl A = Cl {x} ) by ZFMISC_1:31, PRE_TOPC:19, TOPS_1:5; :: thesis: ( ( for x being Point of X st x in A holds

Cl A = Cl {x} ) implies A is anti-discrete )

assume A1: for x being Point of X st x in A holds

Cl A = Cl {x} ; :: thesis: A is anti-discrete

Cl A = Cl {x} ) by ZFMISC_1:31, PRE_TOPC:19, TOPS_1:5; :: thesis: ( ( for x being Point of X st x in A holds

Cl A = Cl {x} ) implies A is anti-discrete )

assume A1: for x being Point of X st x in A holds

Cl A = Cl {x} ; :: thesis: A is anti-discrete

now :: thesis: for x being Point of X st x in A holds

A c= Cl {x}

hence
A is anti-discrete
; :: thesis: verumA c= Cl {x}

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 A1;

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

end;assume x in A ; :: thesis: A c= Cl {x}

then Cl A = Cl {x} by A1;

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