let GX be TopStruct ; :: thesis: for S being Subset of GX st S is boundary & S is closed holds
S is nowhere_dense
let S be Subset of GX; :: thesis: ( S is boundary & S is closed implies S is nowhere_dense )
assume ( S is boundary & S is closed ) ; :: thesis: S is nowhere_dense
then Cl S is boundary by PRE_TOPC:52;
hence S is nowhere_dense by Def5; :: thesis: verum