let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds {x} is anti-discrete
let x be Point of Y; :: thesis: {x} is anti-discrete

now :: thesis: for G being Subset of Y st G is open & {x} meets G holds
{x} c= G

let G be Subset of Y; :: thesis: ( G is open & {x} meets G implies {x} c= G )
assume G is open ; :: thesis: ( {x} meets G implies {x} c= G )
assume {x} meets G ; :: thesis: {x} c= G
then consider a being object such that
A1: a in {x} /\ G by XBOOLE_0:4;
a in {x} by A1, XBOOLE_0:def 4;
then A2: a = x by TARSKI:def 1;
a in G by A1, XBOOLE_0:def 4;
hence {x} c= G by A2, ZFMISC_1:31; :: thesis: verum

end;

hence {x} is anti-discrete ; :: thesis: verum