let X be non empty TopSpace; :: thesis:
let A be Subset of X; :: thesis:
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:

assume A is everywhere_dense ; :: thesis:
then A1: A ` is nowhere_dense by Th39;
let F be Subset of X; :: thesis:
assume F <> the carrier of X ; :: thesis:
then A2: ([#] X) \ F <> {} by PRE_TOPC:4;
assume F is closed ; :: thesis:
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 by A3, SUBSET_1:12;
hence F c= H ; :: thesis:
H ` <> {} by A4;
then ([#] X) \ H <> {} ;
hence H <> the carrier of X by PRE_TOPC:4; :: thesis:
thus H is closed by A5; :: thesis:
(A `) /\ (H `) = {} by A6;
then (A \/ H) ` = {} X by XBOOLE_1:53;
hence A \/ H = the carrier of X by Th2; :: thesis:

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:
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 )

let G be Subset of X; :: thesis:
assume G <> {} ; :: thesis:
then (G `) ` <> {} ;
then A8: G ` <> [#] X by PRE_TOPC:4;
assume G is open ; :: thesis:
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 `) ` by A9, SUBSET_1:12;
hence H c= G ; :: thesis:
F <> [#] X by A10;
hence H <> {} by PRE_TOPC:4; :: thesis:
thus H is open by A11; :: thesis:
(A \/ F) ` = {} X by A12, Th2;
hence (A `) /\ H = {} by XBOOLE_1:53; :: according to XBOOLE_0:def 7 :: thesis:

end;

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