let X be non empty TopSpace; :: thesis: for A being non empty Subset of X st A is boundary holds
not X modified_with_respect_to (A `) is almost_discrete
let A be non empty Subset of X; :: thesis: ( A is boundary implies not X modified_with_respect_to (A `) is almost_discrete )
set Z = X modified_with_respect_to (A `);
assume A1: A is boundary ; :: thesis: not X modified_with_respect_to (A `) is almost_discrete
now :: thesis: ex C being non empty Subset of (X modified_with_respect_to (A `)) st C is nowhere_dense
reconsider C = A as non empty Subset of (X modified_with_respect_to (A `)) by TMAP_1:93;
take C = C; :: thesis: C is nowhere_dense
thus C is nowhere_dense by A1, Th7; :: thesis: verum
end;
hence not X modified_with_respect_to (A `) is almost_discrete ; :: thesis: verum