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 )
assume A2: F is closed ; :: thesis: ( x in F & x in A implies A c= F )
assume A3: x in F ; :: thesis: ( x in A implies A c= F )
assume x in A ; :: thesis: A c= F
then A4: not A /\ F is empty by A3, XBOOLE_0:def 4;
assume not A c= F ; :: thesis: contradiction
then A \ F <> {} by XBOOLE_1:37;
then consider a being set such that
A5: a in A \ F by XBOOLE_0:def 1;
A6: a in A by A5, XBOOLE_0:def 5;
set G = ([#] Y) \ F;
A7: (([#] Y) \ F) ` = (F ` ) `
.= F ;
A8: A \ F c= ([#] Y) \ F by XBOOLE_1:33;
([#] Y) \ F is open by A2, PRE_TOPC:def 6;
then A c= ([#] Y) \ F by A1, A5, A6, A8, Def1;
then ( A misses (([#] Y) \ F) ` & (([#] Y) \ F) ` = F ) by A7, SUBSET_1:44;
hence contradiction by A4, XBOOLE_0:def 7; :: 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

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 )
assume A10: G is open ; :: thesis: ( x in G & x in A implies A c= G )
assume A11: x in G ; :: thesis: ( x in A implies A c= G )
assume A12: 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 set such that
A13: a in A \ G by XBOOLE_0:def 1;
A14: a in A by A13, XBOOLE_0:def 5;
set F = ([#] Y) \ G;
A15: A \ G c= ([#] Y) \ G by XBOOLE_1:33;
G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:22;
then ([#] Y) \ G is closed by A10, PRE_TOPC:def 6;
then A c= ([#] Y) \ G by A9, A13, A14, A15;
then ( A misses (([#] Y) \ G) ` & ([#] Y) \ G = G ` ) by SUBSET_1:44;
hence contradiction by A11, A12, XBOOLE_0:3; :: thesis: verum

end;

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

end;