thus ( A is anti-discrete implies for x being Point of X st x in A holds
A c= Cl {x} ) :: thesis: ( ( for x being Point of X st x in A holds
A c= 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
A c= Cl {x}

let x be Point of X; :: thesis: ( x in A implies A c= Cl {x} )
assume A2: x in A ; :: thesis: A c= Cl {x}
{x} c= Cl {x} by PRE_TOPC:18;
then A3: x in Cl {x} by ZFMISC_1:31;
( A misses Cl {x} or A c= Cl {x} ) by A1;
hence A c= Cl {x} by ; :: thesis: verum
end;
thus ( ( for x being Point of X st x in A holds
A c= Cl {x} ) implies A is anti-discrete ) :: thesis: verum
proof
assume A4: for x being Point of X st x in A holds
A c= Cl {x} ; :: thesis:
now :: thesis: for F being Subset of X st F is closed & A meets F holds
A c= F
let F be Subset of X; :: thesis: ( F is closed & A meets F implies A c= F )
assume A5: F is closed ; :: thesis: ( A meets F implies A c= F )
assume A meets F ; :: thesis: A c= F
then consider a being object such that
A6: a in A /\ F by XBOOLE_0:4;
reconsider a = a as Point of X by A6;
a in F by ;
then {a} c= F by ZFMISC_1:31;
then A7: Cl {a} c= F by ;
a in A by ;
then A c= Cl {a} by A4;
hence A c= F by A7; :: thesis: verum
end;
hence A is anti-discrete ; :: thesis: verum
end;