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

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 set such that
A1: a in {x} /\ G by XBOOLE_0:4;
( a in {x} & a in G ) by A1, XBOOLE_0:def 4;
then ( a = x & {a} c= G ) by TARSKI:def 1, ZFMISC_1:37;
hence {x} c= G ; :: thesis: verum

end;

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