let X be non empty TopSpace; :: thesis: for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty open SubSpace of X; :: thesis: for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let A, C be Subset of X; :: thesis: for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; :: thesis: ( C = the carrier of X0 & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C = the carrier of X0 ; :: thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A = B ; :: thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
C is open by A1, TSEP_1:def 1;
hence ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) by A1, A2, Th62; :: thesis: verum