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} ) by ZFMISC_1:31, TOPS_1:5; :: thesis: ( ( for x being Point of X st x in A holds

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

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

( ( 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} ) by ZFMISC_1:31, TOPS_1:5; :: thesis: ( ( for x being Point of X st x in A holds

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

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 A1:
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 ; :: thesis: A is closed

end;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 ; :: thesis: A is closed