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 )

A c= Cl {x} ) implies A is anti-discrete ) :: thesis: verum

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

thus
( ( for x being Point of X st x in A holds
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 A2, A3, XBOOLE_0:3; :: thesis: verum

end;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 A2, A3, XBOOLE_0:3; :: thesis: verum

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: A is anti-discrete

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

now :: thesis: for F being Subset of X st F is closed & A meets F holds

A c= F

hence
A is anti-discrete
; :: thesis: verumA 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 A6, XBOOLE_0:def 4;

then {a} c= F by ZFMISC_1:31;

then A7: Cl {a} c= F by A5, TOPS_1:5;

a in A by A6, XBOOLE_0:def 4;

then A c= Cl {a} by A4;

hence A c= F by A7; :: thesis: verum

end;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 A6, XBOOLE_0:def 4;

then {a} c= F by ZFMISC_1:31;

then A7: Cl {a} c= F by A5, TOPS_1:5;

a in A by A6, XBOOLE_0:def 4;

then A c= Cl {a} by A4;

hence A c= F by A7; :: thesis: verum