set Y0 = the non empty trivial strict SubSpace of Y;
take the non empty trivial strict SubSpace of Y ; :: thesis: ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict )
thus ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict ) ; :: thesis: verum