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 closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
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 closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X ) )
assume D is everywhere_dense ; :: thesis: ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
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 closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; :: thesis: ( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus ( C is open & C is dense & B is closed & B is boundary ) by A2, Th18; :: thesis: ( C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus C \/ (D /\ B) = (C \/ D) /\ (C \/ (C `)) by XBOOLE_1:24
.= (C \/ D) /\ ([#] X) by PRE_TOPC:2
.= C \/ D by XBOOLE_1:28
.= D by A1, XBOOLE_1:12 ; :: thesis: ( C misses B & C \/ B = the carrier of X )
C misses B by XBOOLE_1:79;
hence C /\ B = {} ; :: according to XBOOLE_0:def 7 :: thesis: C \/ B = the carrier of X
C \/ B = [#] X by PRE_TOPC:2;
hence C \/ B = the carrier of X ; :: thesis: verum