let GX be TopStruct ; :: thesis: for R, S being Subset of GX st R is dense & R c= S holds
S is dense
let R, S be Subset of GX; :: thesis: ( R is dense & R c= S implies S is dense )
assume that
A1: R is dense and
A2: R c= S ; :: thesis: S is dense
Cl R = [#] GX by A1;
then [#] GX c= Cl S by A2, PRE_TOPC:19;
then [#] GX = Cl S ;
hence S is dense ; :: thesis: verum