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 G being Subset of Y st
( G is open & A /\ G = {x} )
let A be Subset of Y; :: thesis: ( A is discrete implies for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} ) )
assume A1: A is discrete ; :: thesis: for x being Point of Y st x in A holds
ex G being Subset of Y st
( G is open & A /\ G = {x} )
let x be Point of Y; :: thesis: ( x in A implies ex G being Subset of Y st
( G is open & A /\ G = {x} ) )
assume A2: x in A ; :: thesis: ex G being Subset of Y st
( G is open & A /\ G = {x} )
then reconsider Y9 = Y as non empty TopStruct ;
reconsider B = {x} as Subset of Y9 by ZFMISC_1:31;
reconsider A9 = A as Subset of Y9 ;
{x} c= A9 by A2, ZFMISC_1:31;
then consider G being Subset of Y9 such that
A3: G is open and
A4: A9 /\ G = B by A1;
reconsider G = G as Subset of Y ;
take G ; :: thesis: ( G is open & A /\ G = {x} )
thus ( G is open & A /\ G = {x} ) by A3, A4; :: thesis: verum