let X be non empty TopSpace; :: thesis: for D being Subset of X
for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds
C is everywhere_dense
let D be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds
C is everywhere_dense
let C be Subset of (X modified_with_respect_to D); :: thesis: ( D c= C & D is dense implies C is everywhere_dense )
assume A1: D c= C ; :: thesis: ( not D is dense or C is everywhere_dense )
assume A2: D is dense ; :: thesis: C is everywhere_dense
reconsider E = D as Subset of (X modified_with_respect_to D) by TMAP_1:104;
( E is dense & E is open ) by A2, Th4;
hence C is everywhere_dense by A1, TOPS_3:36, TOPS_3:38; :: thesis: verum