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

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

hence
{x} is anti-discrete
; :: thesis: verum{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;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