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

Int C c= C by TOPS_1:16;
then reconsider D = Int C as Subset of X0 by A1, XBOOLE_1:1;
A4: D /\ B c= Int C by XBOOLE_1:17;
then reconsider E = D /\ B as Subset of X by XBOOLE_1:1;
assume A5: C is everywhere_dense ; :: thesis: ( not B is everywhere_dense or A is everywhere_dense )
then Int C is everywhere_dense ;
then A6: D is everywhere_dense by Th61;
assume B is everywhere_dense ; :: thesis: A is everywhere_dense
then A7: D /\ B is everywhere_dense by A6, Th44;
Int C is dense by A5;
then E is everywhere_dense by A7, A4, 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