hereby :: thesis: ( ( for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F ) implies A is anti-discrete )

assume A1: A is anti-discrete ; :: thesis: for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F
let x be Point of Y; :: thesis: for F being Subset of Y st F is closed & x in F & x in A holds
A c= F
let F be Subset of Y; :: thesis: ( F is closed & x in F & x in A implies A c= F )
set G = ([#] Y) \ F;
A2: A \ F c= ([#] Y) \ F by XBOOLE_1:33;
assume F is closed ; :: thesis: ( x in F & x in A implies A c= F )
then A3: ([#] Y) \ F is open by PRE_TOPC:def 3;
assume A4: x in F ; :: thesis: ( x in A implies A c= F )
assume A5: x in A ; :: thesis: A c= F
assume not A c= F ; :: thesis: contradiction
then A \ F <> {} by XBOOLE_1:37;
then consider a being object such that
A6: a in A \ F by XBOOLE_0:def 1;
a in A by A6, XBOOLE_0:def 5;
then A c= ([#] Y) \ F by A1, A6, A2, A3;
then A7: A misses (([#] Y) \ F) ` by SUBSET_1:24;
A8: (([#] Y) \ F) ` = (F `) `
.= F ;
not A /\ F is empty by A4, A5, XBOOLE_0:def 4;
hence contradiction by A8, A7; :: thesis: verum

end;

hereby :: thesis: verum

assume A9: for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F ; :: thesis: A is anti-discrete

now :: thesis: 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

let x be Point of Y; :: thesis: for G being Subset of Y st G is open & x in G & x in A holds
A c= G
let G be Subset of Y; :: thesis: ( G is open & x in G & x in A implies A c= G )
set F = ([#] Y) \ G;
A10: A \ G c= ([#] Y) \ G by XBOOLE_1:33;
A11: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3;
assume G is open ; :: thesis: ( x in G & x in A implies A c= G )
then A12: ([#] Y) \ G is closed by A11, PRE_TOPC:def 3;
assume A13: x in G ; :: thesis: ( x in A implies A c= G )
assume A14: x in A ; :: thesis: A c= G
assume not A c= G ; :: thesis: contradiction
then A \ G <> {} by XBOOLE_1:37;
then consider a being object such that
A15: a in A \ G by XBOOLE_0:def 1;
A16: ([#] Y) \ G = G ` ;
a in A by A15, XBOOLE_0:def 5;
then A c= ([#] Y) \ G by A9, A15, A10, A12;
then A misses (([#] Y) \ G) ` by SUBSET_1:24;
hence contradiction by A13, A14, A16, XBOOLE_0:3; :: thesis: verum

end;

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

end;