let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
let A be Subset of X; :: thesis: ( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds
A = Cl {x} )
thus ( A is anti-discrete & A is closed implies for x being Point of X st x in A holds
A = Cl {x} ) :: thesis: ( ( for x being Point of X st x in A holds
A = Cl {x} ) implies ( A is anti-discrete & A is closed ) )

proof

assume A1: A is anti-discrete ; :: thesis: ( not A is closed or for x being Point of X st x in A holds
A = Cl {x} )
assume A2: A is closed ; :: thesis: for x being Point of X st x in A holds
A = Cl {x}
let x be Point of X; :: thesis: ( x in A implies A = Cl {x} )
assume A3: x in A ; :: thesis: A = Cl {x}
then {x} c= A by ZFMISC_1:31;
then A4: Cl {x} c= A by A2, TOPS_1:5;
A c= Cl {x} by A1, A3, Def12;
hence A = Cl {x} by A4, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( ( for x being Point of X st x in A holds
A = Cl {x} ) implies ( A is anti-discrete & A is closed ) ) :: thesis: verum

proof

assume A5: for x being Point of X st x in A holds
A = Cl {x} ; :: thesis: ( A is anti-discrete & A is closed )
then for x being Point of X st x in A holds
A c= Cl {x} ;
hence A is anti-discrete by Def12; :: thesis: A is closed

hereby :: thesis: verum

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: A is closed

hence A is closed ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: A is closed

then consider a being set such that
A6: a in A by XBOOLE_0:def 1;
reconsider a = a as Point of X by A6;
A = Cl {a} by A5, A6;
hence A is closed ; :: thesis: verum

end;

end;

end;

end;