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