let Y0 be non empty SubSpace of Y; :: thesis: ( Y0 is maximal_discrete implies Y0 is discrete )
assume A1: Y0 is maximal_discrete ; :: thesis: Y0 is discrete
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
A is maximal_discrete by A1, Def8;
then A is discrete by Def7;
hence Y0 is discrete by Th26; :: thesis: verum