let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let A be Subset of X; :: thesis: for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let B be Subset of X0; :: thesis: ( A c= B & A is everywhere_dense implies B is everywhere_dense )
assume A1: A c= B ; :: thesis: ( not A is everywhere_dense or B is everywhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is everywhere_dense ; :: thesis: B is everywhere_dense
then Int A is dense ;
then Int C is dense by Th56, Th59;
then Int B is dense by A1, TOPS_1:19, TOPS_1:44;
hence B is everywhere_dense ; :: thesis: verum