let Y0 be non empty SubSpace of Y; :: thesis: ( Y0 is trivial implies Y0 is proper )
assume Y0 is trivial ; :: thesis: Y0 is proper
then for A being Subset of Y st A = the carrier of Y0 holds
A is proper ;
hence Y0 is proper by Def3; :: thesis: verum