let X be non empty TopSpace; :: thesis: for A being Subset of X st A is discrete holds
for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
let A be Subset of X; :: thesis: ( A is discrete implies for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} )
assume A1: A is discrete ; :: thesis: for x being Point of X st x in A holds
A /\ (Cl {x}) = {x}
let x be Point of X; :: thesis: ( x in A implies A /\ (Cl {x}) = {x} )
assume x in A ; :: thesis: A /\ (Cl {x}) = {x}
then {x} c= A by ZFMISC_1:31;
hence A /\ (Cl {x}) = {x} by A1, Th41; :: thesis: verum