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

let D be Subset of X; :: thesis: ( D c= {x} implies ex G being Subset of X st
( G is open & {x} /\ G = D ) )
assume A1: D c= {x} ; :: thesis: ex G being Subset of X st
( G is open & {x} /\ G = D )

A2: now

assume A3: D = {} ; :: thesis: ex G being Element of K10(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 A3; :: thesis: verum

end;

end;

now

assume A4: D = {x} ; :: thesis: ex G being Element of K10(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;

hence ex G being Subset of X st
( G is open & {x} /\ G = D ) by A1, A2, ZFMISC_1:39; :: thesis: verum

end;

hence {x} is discrete by Def5; :: thesis: verum