let X0 be non empty SubSpace of X; :: thesis: ( X0 is maximal_discrete implies not X0 is trivial )
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
assume X0 is maximal_discrete ; :: thesis: not X0 is trivial
then A is maximal_discrete ;
then A is dense by Th56;
then A1: Cl A = the carrier of X by TOPS_3:def 2;
assume X0 is trivial ; :: thesis: contradiction
then consider s being Element of X0 such that
A2: the carrier of X0 = {s} by SUBSET_1:46;
s in A ;
then reconsider a = s as Point of X ;
A = {a} by A2;
then for C being Subset of X
for x being Point of X st C = {x} holds
Cl C = the carrier of X by A1, Th49;
hence contradiction by TDLAT_3:20; :: thesis: verum