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

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 by Def3; :: thesis: verum