let X be non empty non almost_discrete TopSpace; :: thesis: for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
let X0 be non empty everywhere_dense SubSpace of X; :: thesis: ( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: B is nowhere_dense and
A3: C \/ B = D and
A4: C misses B by TOPS_3:49;
C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A5: C = the carrier of X1 by A1, Th23;
assume A6: ( not X0 is dense or not X0 is open ) ; :: thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
now :: thesis: C is proper
assume not C is proper ; :: thesis: contradiction
then A7: C = the carrier of X by SUBSET_1:def 6;
C c= D by A3, XBOOLE_1:7;
then D = [#] X by A7, XBOOLE_0:def 10;
then ( D is dense & D is open ) ;
hence contradiction by A6, TSEP_1:16; :: thesis: verum
end;
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A5, TEX_2:8;
now :: thesis: not B = {}
per cases ( not X0 is dense or not X0 is open ) by A6;
end;
end;
then consider X2 being non empty strict nowhere_dense SubSpace of X such that
A10: B = the carrier of X2 by A2, Th62;
take X1 ; :: thesis: ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
take X2 ; :: thesis: ( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
thus X1 misses X2 by A4, A5, A10, TSEP_1:def 3; :: thesis: X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #)
the carrier of (X1 union X2) = the carrier of X0 by A3, A5, A10, TSEP_1:def 2;
hence X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:5; :: thesis: verum