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 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;
assume A5: for G being Subset of Y holds
( 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