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 )

( 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;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

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

end;( 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

hence
A is anti-discrete
; :: thesis: verumA 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;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