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 C c= D & D is boundary holds
C is nowhere_dense
let D be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to (D ` )) st C c= D & D is boundary holds
C is nowhere_dense
let C be Subset of (X modified_with_respect_to (D ` )); :: thesis: ( C c= D & D is boundary implies C is nowhere_dense )
assume A1: C c= D ; :: thesis: ( not D is boundary or C is nowhere_dense )
assume A2: D is boundary ; :: thesis: C is nowhere_dense
reconsider E = D as Subset of (X modified_with_respect_to (D ` )) by TMAP_1:104;
( E is boundary & E is closed ) by A2, Th6;
hence C is nowhere_dense by A1, TOPS_3:26; :: thesis: verum