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
ex A being Subset of Y st
( A = the carrier of Y0 & not A is proper ) by Def3;
then reconsider A = the carrier of Y0 as non empty Subset of Y ;
A is trivial ;
hence Y0 is trivial ; :: thesis: verum