let Y0 be SubSpace of X; :: thesis: ( Y0 is maximal_discrete implies not Y0 is proper )
reconsider A = the carrier of Y0 as Subset of X by Lm1;
assume Y0 is maximal_discrete ; :: thesis: not Y0 is proper
then A1: A is maximal_discrete ;
( A = the carrier of Y0 & not A is proper ) by A1, Th43;
hence not Y0 is proper ; :: thesis: verum