let Y0 be non empty SubSpace of X; :: thesis: ( Y0 is trivial implies Y0 is maximal_discrete )
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