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