hereby :: thesis: ( ( for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) ) implies A is anti-discrete )
assume A1: A is anti-discrete ; :: thesis: for G being Subset of Y st G is closed & A meets G holds
A c= G
let G be Subset of Y; :: thesis: ( G is closed & A meets G implies A c= G )
assume G is closed ; :: thesis: ( A meets G implies A c= G )
then ([#] Y) \ G is open by PRE_TOPC:def 3;
then A2: ( A misses G ` or A c= G ` ) by A1;
assume A meets G ; :: thesis: A c= G
then A c= (G `) ` by A2, SUBSET_1:23;
hence A c= G ; :: thesis: verum
end;
hereby :: thesis: verum
assume A3: for G being Subset of Y holds
( not G is closed or A misses G or A c= G ) ; :: thesis: A is anti-discrete
now :: 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 )
A4: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3;
assume G is open ; :: thesis: ( A meets G implies A c= G )
then ([#] Y) \ G is closed by A4, PRE_TOPC:def 3;
then A5: ( A misses G ` or A c= G ` ) by A3;
assume A meets G ; :: thesis: A c= G
then A c= (G `) ` by A5, SUBSET_1:23;
hence A c= G ; :: thesis: verum
end;
hence A is anti-discrete ; :: thesis: verum
end;