let X0 be non empty SubSpace of X; :: thesis: not X0 is nowhere_dense
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
not A is nowhere_dense by TEX_1:def 6;
hence not X0 is nowhere_dense ; :: thesis: verum