let X be non empty TopSpace; :: thesis: for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
let D be Subset of X; :: thesis: ( D is everywhere_dense implies ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B ) )
assume D is everywhere_dense ; :: thesis: ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
then consider C being Subset of X such that
A1: C c= D and
A2: ( C is open & C is dense ) by Th41;
take C ; :: thesis: ex B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
take B = D \ C; :: thesis: ( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
thus ( C is open & C is dense ) by A2; :: thesis: ( B is nowhere_dense & C \/ B = D & C misses B )
C is everywhere_dense by A2, Th36;
then C ` is nowhere_dense by Th39;
hence B is nowhere_dense by Th26, XBOOLE_1:33; :: thesis: ( C \/ B = D & C misses B )
thus ( C \/ B = D & C misses B ) by A1, XBOOLE_1:45, XBOOLE_1:79; :: thesis: verum