let Y be TopStruct ; :: thesis: for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
let A be Subset of Y; :: thesis: ( A is discrete implies for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} ) )
assume A1: A is discrete ; :: thesis: for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )
let x be Point of Y; :: thesis: ( x in A implies ex F being Subset of Y st
( F is closed & A /\ F = {x} ) )
assume A2: x in A ; :: thesis: ex F being Subset of Y st
( F is closed & A /\ F = {x} )
then reconsider Y' = Y as non empty TopStruct ;
reconsider A' = A as Subset of Y' ;
reconsider B = {x} as Subset of Y' by ZFMISC_1:37;
{x} c= A' by A2, ZFMISC_1:37;
then consider F being Subset of Y such that
A3: ( F is closed & A' /\ F = B ) by A1, Def6;
take F ; :: thesis: ( F is closed & A /\ F = {x} )
thus ( F is closed & A /\ F = {x} ) by A3; :: thesis: verum