let Y0 be non empty SubSpace of X; :: thesis: ( Y0 is trivial implies Y0 is maximal_discrete )
reconsider A = the carrier of Y0 as non empty Subset of X by Lm1;
assume Y0 is trivial ; :: thesis: Y0 is maximal_discrete
then for A being Subset of X st A = the carrier of Y0 holds
A is maximal_discrete by Th50;
hence Y0 is maximal_discrete by Def8; :: thesis: verum