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 )
assume A1: 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 & [#] X0 c= [#] X ) by PRE_TOPC:def 9, TOPS_1:def 3;
then [#] X0 = (Cl A) /\ ([#] X0) by XBOOLE_1:28;
then Cl C = [#] X0 by PRE_TOPC:47;
then C is dense by TOPS_1:def 3;
hence B is dense by A1, TOPS_1:79; :: thesis: verum