let Y0 be non empty SubSpace of Y; :: thesis: not Y0 is proper
reconsider A = the carrier of Y0 as non empty Subset of Y by Lm1;

now :: thesis: ex A being non empty Subset of Y st
( A = the carrier of Y0 & not A is proper )

take A = A; :: thesis: ( A = the carrier of Y0 & not A is proper )
thus ( A = the carrier of Y0 & not A is proper ) ; :: thesis: verum

end;

hence not Y0 is proper ; :: thesis: verum