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 that
A1: S is boundary and
A2: S is closed ; :: thesis: S is nowhere_dense
Cl S is boundary by A1, A2, PRE_TOPC:52;
hence S is nowhere_dense by Def5; :: thesis: verum