thus ( A is anti-discrete implies for x being Point of X st x in A holds
Cl A = Cl {x} ) by ZFMISC_1:31, PRE_TOPC:19, TOPS_1:5; :: thesis: ( ( for x being Point of X st x in A holds
Cl A = Cl {x} ) implies A is anti-discrete )
assume A1: for x being Point of X st x in A holds
Cl A = Cl {x} ; :: thesis: A is anti-discrete
now :: 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 x in A ; :: thesis: A c= Cl {x}
then Cl A = Cl {x} by A1;
hence A c= Cl {x} by PRE_TOPC:18; :: thesis: verum
end;
hence A is anti-discrete ; :: thesis: verum