let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let X0 be SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let A be Subset of X; :: thesis: for B being Subset of X0 st A c= B & A is dense holds
B is dense
let B be Subset of X0; :: thesis: ( A c= B & A is dense implies B is dense )
A1: [#] X0 c= [#] X by PRE_TOPC:def 4;
assume A2: A c= B ; :: thesis: ( not A is dense or B is dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume A is dense ; :: thesis: B is dense
then Cl A = [#] X ;
then [#] X0 = (Cl A) /\ ([#] X0) by A1, XBOOLE_1:28;
then Cl C = [#] X0 by PRE_TOPC:17;
then C is dense ;
hence B is dense by A2, TOPS_1:44; :: thesis: verum