hereby :: thesis: ( ( for G being Subset of Y holds

( not G is open or A misses G or A c= G ) ) implies A is anti-discrete )

assume A5:
for G being Subset of Y holds ( not G is open or A misses G or A c= G ) ) implies A is anti-discrete )

assume A1:
A is anti-discrete
; :: thesis: for G being Subset of Y st G is open & A meets G holds

A c= G

let G be Subset of Y; :: thesis: ( G is open & A meets G implies A c= G )

assume A2: G is open ; :: thesis: ( A meets G implies A c= G )

assume A meets G ; :: thesis: A c= G

then consider a being object such that

A3: a in A /\ G by XBOOLE_0:4;

reconsider a = a as Point of Y by A3;

A4: a in G by A3, XBOOLE_0:def 4;

a in A by A3, XBOOLE_0:def 4;

hence A c= G by A1, A2, A4; :: thesis: verum

end;A c= G

let G be Subset of Y; :: thesis: ( G is open & A meets G implies A c= G )

assume A2: G is open ; :: thesis: ( A meets G implies A c= G )

assume A meets G ; :: thesis: A c= G

then consider a being object such that

A3: a in A /\ G by XBOOLE_0:4;

reconsider a = a as Point of Y by A3;

A4: a in G by A3, XBOOLE_0:def 4;

a in A by A3, XBOOLE_0:def 4;

hence A c= G by A1, A2, A4; :: thesis: verum

( not G is open or A misses G or A c= G ) ; :: thesis: A is anti-discrete

for x being Point of Y

for G being Subset of Y st G is open & x in G & x in A holds

A c= G by A5, XBOOLE_0:3;

hence A is anti-discrete ; :: thesis: verum