let X be non empty TopSpace; :: thesis: for x being Point of X holds {x} is discrete
let x be Point of X; :: thesis: {x} is discrete
now :: thesis: for D being Subset of X st D c= {x} holds
ex G being Subset of X st
( G is open & {x} /\ G = D )
let D be Subset of X; :: thesis: ( D c= {x} implies ex G being Subset of X st
( G is open & {x} /\ G = D ) )
A1: now :: thesis: ( D = {} implies ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D ) )
assume A2: D = {} ; :: thesis: ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D )
hereby :: thesis: verum
take G = {} X; :: thesis: ( G is open & {x} /\ G = D )
thus ( G is open & {x} /\ G = D ) by A2; :: thesis: verum
end;
end;
A3: now :: thesis: ( D = {x} implies ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D ) )
assume A4: D = {x} ; :: thesis: ex G being Element of bool the carrier of X st
( G is open & {x} /\ G = D )
hereby :: thesis: verum
take G = [#] X; :: thesis: ( G is open & {x} /\ G = D )
thus ( G is open & {x} /\ G = D ) by A4, XBOOLE_1:28; :: thesis: verum
end;
end;
assume D c= {x} ; :: thesis: ex G being Subset of X st
( G is open & {x} /\ G = D )
hence ex G being Subset of X st
( G is open & {x} /\ G = D ) by A1, A3, ZFMISC_1:33; :: thesis: verum
end;
hence {x} is discrete ; :: thesis: verum