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