let Y0 be non empty SubSpace of Y; :: thesis: ( not Y0 is proper implies Y0 is trivial )
assume not Y0 is proper ; :: thesis: Y0 is trivial
consider A being Subset of Y such that
A1: A = the carrier of Y0 and
not A is proper by Def3;
reconsider A = the carrier of Y0 as non empty Subset of Y by A1;
A is trivial ;
hence Y0 is trivial ; :: thesis: verum