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 )

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

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

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

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