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 )
reconsider E = D as Subset of (X modified_with_respect_to (D `)) by TMAP_1:93;
assume A2: D is boundary ; :: thesis: C is nowhere_dense
then A3: E is closed by Th6;
E is boundary by A2, Th6;
hence C is nowhere_dense by A1, A3, TOPS_3:26; :: thesis: verum