let X be non empty non almost_discrete TopSpace; 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; ( ( 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 )
; 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 #) )
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A5, TEX_2:8;
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
; 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
; ( 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; 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; verum