let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
let A be Subset of X; :: thesis: ( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
thus ( A is everywhere_dense implies for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) :: thesis: ( ( for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) implies A is everywhere_dense )

proof

assume A is everywhere_dense ; :: thesis: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then A1: A ` is nowhere_dense by Th39;
let F be Subset of X; :: thesis: ( F <> the carrier of X & F is closed implies ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
assume F <> the carrier of X ; :: thesis: ( not F is closed or ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
then A2: ([#] X) \ F <> {} by PRE_TOPC:4;
assume F is closed ; :: thesis: ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then consider G being Subset of X such that
A3: G c= F ` and
A4: G <> {} and
A5: G is open and
A6: A ` misses G by A1, A2, Th28;
take H = G ` ; :: thesis: ( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
(F `) ` c= H by A3, SUBSET_1:12;
hence F c= H ; :: thesis: ( H <> the carrier of X & H is closed & A \/ H = the carrier of X )
H ` <> {} by A4;
then ([#] X) \ H <> {} ;
hence H <> the carrier of X by PRE_TOPC:4; :: thesis: ( H is closed & A \/ H = the carrier of X )
thus H is closed by A5; :: thesis: A \/ H = the carrier of X
(A `) /\ (H `) = {} by A6;
then (A \/ H) ` = {} X by XBOOLE_1:53;
hence A \/ H = the carrier of X by Th2; :: thesis: verum

end;

assume A7: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ; :: thesis: A is everywhere_dense
for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )

proof

let G be Subset of X; :: thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
assume G <> {} ; :: thesis: ( not G is open or ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
then (G `) ` <> {} ;
then A8: G ` <> [#] X by PRE_TOPC:4;
assume G is open ; :: thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )
then consider F being Subset of X such that
A9: G ` c= F and
A10: F <> the carrier of X and
A11: F is closed and
A12: A \/ F = the carrier of X by A7, A8;
take H = F ` ; :: thesis: ( H c= G & H <> {} & H is open & A ` misses H )
H c= (G `) ` by A9, SUBSET_1:12;
hence H c= G ; :: thesis: ( H <> {} & H is open & A ` misses H )
F <> [#] X by A10;
hence H <> {} by PRE_TOPC:4; :: thesis: ( H is open & A ` misses H )
thus H is open by A11; :: thesis: A ` misses H
(A \/ F) ` = {} X by A12, Th2;
hence (A `) /\ H = {} by XBOOLE_1:53; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

then A ` is nowhere_dense by Th28;
hence A is everywhere_dense by Th39; :: thesis: verum