let X be non empty TopSpace; :: thesis: for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
let D be Subset of X; :: thesis: ( D is nowhere_dense implies ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X ) )
assume D is nowhere_dense ; :: thesis: ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: D c= C and
A2: ( C is closed & C is boundary ) by Th27;
take C ; :: thesis: ex B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
take B = D \/ (C `); :: thesis: ( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
thus ( C is closed & C is boundary ) by A2; :: thesis: ( B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
C ` is everywhere_dense by A2, Th40;
hence B is everywhere_dense by Th38, XBOOLE_1:7; :: thesis: ( C /\ B = D & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ B = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3
.= D by A1, XBOOLE_1:28 ; :: thesis: C \/ B = the carrier of X
thus C \/ B = D \/ (C \/ (C `)) by XBOOLE_1:4
.= D \/ ([#] X) by PRE_TOPC:2
.= the carrier of X by XBOOLE_1:12 ; :: thesis: verum