let X0 be SubSpace of X; :: thesis: ( X0 is maximal_T_0 implies X0 is dense )
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is maximal_T_0 ; :: thesis: X0 is dense
then A is maximal_T_0 ;
then A is dense by Th2;
hence X0 is dense by TEX_3:9; :: thesis: verum