let X0 be SubSpace of X; :: thesis: ( X0 is nowhere_dense implies not X0 is dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense ; :: thesis: not X0 is dense
then A is nowhere_dense ;
then A2: not A is dense by TOPS_3:25;
assume X0 is dense ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum