let X0 be SubSpace of X; :: thesis: ( X0 is proper implies not X0 is everywhere_dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is proper ; :: thesis: not X0 is everywhere_dense
then A is proper by TEX_2:8;
then A <> the carrier of X by SUBSET_1:def 6;
then not A is everywhere_dense by TEX_1:32;
hence not X0 is everywhere_dense ; :: thesis: verum