let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X st ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) holds
A is discrete
let A be Subset of X; :: thesis: ( ( for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
A /\ (Cl {x}) = {x} ; :: thesis: A is discrete
now :: thesis: for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} )
let x be Point of X; :: thesis: ( x in A implies ex F being Subset of X st
( F is closed & A /\ F = {x} ) )
assume A2: x in A ; :: thesis: ex F being Subset of X st
( F is closed & A /\ F = {x} )
now :: thesis: ex F being Element of bool the carrier of X st
( F is closed & A /\ F = {x} )
take F = Cl {x}; :: thesis: ( F is closed & A /\ F = {x} )
thus F is closed ; :: thesis: A /\ F = {x}
thus A /\ F = {x} by A1, A2; :: thesis: verum
end;
hence ex F being Subset of X st
( F is closed & A /\ F = {x} ) ; :: thesis: verum
end;
hence A is discrete by Th51; :: thesis: verum