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
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
hereby :: thesis: verum
per cases ( A is empty or not A is empty ) ;
suppose not A is empty ; :: thesis: A is closed
then consider a being object such that
A2: a in A ;
reconsider a = a as Point of X by A2;
A = Cl {a} by A1, A2;
hence A is closed ; :: thesis: verum
end;
end;
end;
end;