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 open & B is dense & C /\ (D \/ B) = D & C misses B & 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 open & B is dense & C /\ (D \/ B) = D & C misses B & 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 open & B is dense & C /\ (D \/ B) = D & C misses B & 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 open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; :: thesis: ( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
thus ( C is closed & C is boundary & B is open & B is dense ) by A2; :: thesis: ( C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ (D \/ B) = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3
.= D by A1, XBOOLE_1:28 ; :: 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