let X0 be SubSpace of X; :: thesis: ( X0 is nowhere_dense implies X0 is boundary )
assume A1: X0 is nowhere_dense ; :: thesis: X0 is boundary
now :: thesis: for A being Subset of X st A = the carrier of X0 holds
A is boundary
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is boundary )
assume A = the carrier of X0 ; :: thesis: A is boundary
then A is nowhere_dense by A1;
hence A is boundary ; :: thesis: verum
end;
hence X0 is boundary ; :: thesis: verum