consider Y0 being non empty trivial strict SubSpace of Y;
take Y0 ; :: thesis: ( Y0 is proper & Y0 is trivial & Y0 is strict )
thus ( Y0 is proper & Y0 is trivial & Y0 is strict ) ; :: thesis: verum