let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; :: thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C c= the carrier of X0 ; :: thesis: ( not A c= C or not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A c= C ; :: thesis: ( not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A3: A = B ; :: thesis: ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
thus ( C is everywhere_dense & B is everywhere_dense implies A is everywhere_dense ) :: thesis: ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) )

proof

assume A4: C is everywhere_dense ; :: thesis: ( not B is everywhere_dense or A is everywhere_dense )
then A5: Int C is everywhere_dense by Th32;
A6: ( Int C is dense & Int C is open ) by A4, Th32, Th33;
Int C c= C by TOPS_1:44;
then reconsider D = Int C as Subset of X0 by A1, XBOOLE_1:1;
assume A7: B is everywhere_dense ; :: thesis: A is everywhere_dense
D is everywhere_dense by A5, Th61;
then A8: D /\ B is everywhere_dense by A7, Th44;
A9: D /\ B c= Int C by XBOOLE_1:17;
then reconsider E = D /\ B as Subset of X by XBOOLE_1:1;
E is everywhere_dense by A6, A8, A9, Th62;
hence A is everywhere_dense by A3, Th38, XBOOLE_1:17; :: thesis: verum

end;

thus ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) ) by A2, A3, Th38, Th61; :: thesis: verum