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
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ) holds
A is discrete
let A be Subset of X; :: 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} ) ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
ex F being Subset of X st
( F is closed & A /\ F = {x} ) ; :: thesis: A is discrete
now :: thesis: for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} )
let x be Point of X; :: thesis: ( x in A implies ex G being Subset of X st
( G is open & A /\ G = {x} ) )
assume A2: x in A ; :: thesis: ex G being Subset of X st
( G is open & A /\ G = {x} )
now :: thesis: ex F being Subset of X st
( F is open & A /\ F = {x} )
consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = {x} by A1, A2;
take F = F; :: thesis: ( F is open & A /\ F = {x} )
thus F is open by A3, TDLAT_3:22; :: thesis: A /\ F = {x}
thus A /\ F = {x} by A4; :: thesis: verum
end;
hence ex G being Subset of X st
( G is open & A /\ G = {x} ) ; :: thesis: verum
end;
hence A is discrete by Th31; :: thesis: verum