let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is everywhere_dense & A c= B holds
B is everywhere_dense
let A, B be Subset of X; :: thesis: ( A is everywhere_dense & A c= B implies B is everywhere_dense )
assume A is everywhere_dense ; :: thesis: ( not A c= B or B is everywhere_dense )
then A1: Cl (Int A) = [#] X ;
assume A c= B ; :: thesis: B is everywhere_dense
then Int A c= Int B by TOPS_1:19;
then Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
then [#] X = Cl (Int B) by A1;
hence B is everywhere_dense ; :: thesis: verum