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 is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is 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 is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is 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 is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; :: thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C is open ; :: thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume C c= the carrier of X0 ; :: thesis: ( not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
then reconsider E = C as Subset of X0 ;
A2: E is open by A1, TOPS_2:25;
assume A3: A c= C ; :: thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A4: A = B ; :: thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
Int B c= Int E by A3, A4, TOPS_1:19;
then A6: Int B c= E by A2, TOPS_1:23;
then A7: D is open by A1, TSEP_1:9;
thus ( C is dense & B is everywhere_dense implies A is everywhere_dense ) :: thesis: ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) )
proof
assume A8: C is dense ; :: thesis: ( not B is everywhere_dense or A is everywhere_dense )
assume B is everywhere_dense ; :: thesis: A is everywhere_dense
then Int B is dense ;
then D is dense by A6, A8, Th60;
then Int A is dense by A4, A5, A7, TOPS_1:24, TOPS_1:44;
hence A is everywhere_dense ; :: thesis: verum
end;
thus ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) ) by A3, Th33, Th38, A4, Th61; :: thesis: verum