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 )
reconsider E = D as Subset of (X modified_with_respect_to D) by TMAP_1:93;
assume A2: D is dense ; :: thesis: C is everywhere_dense
then A3: E is open by Th4;
E is dense by A2, Th4;
hence C is everywhere_dense by A1, A3, TOPS_3:36, TOPS_3:38; :: thesis: verum