let X be non empty TopSpace; :: thesis: for D being Subset of
for C being Subset of st D c= C & D is dense holds
C is everywhere_dense
let D be Subset of ; :: thesis: for C being Subset of st D c= C & D is dense holds
C is everywhere_dense
let C be Subset of ; :: 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 by TMAP_1:104;
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