let GX be TopStruct ; :: thesis: for R being Subset of GX st R is nowhere_dense holds
R is boundary
let R be Subset of GX; :: thesis: ( R is nowhere_dense implies R is boundary )
assume R is nowhere_dense ; :: thesis: R is boundary
then R ` is dense by Th91;
hence R is boundary by Def4; :: thesis: verum