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:13;
then A <> the carrier of X by SUBSET_1:def 7;
then not A is everywhere_dense by TEX_1:36;
hence not X0 is everywhere_dense by Th16; :: thesis: verum