take Y0 = the non empty trivial SubSpace of Y; :: thesis: Y0 is 1 -element
thus Y0 is 1 -element ; :: thesis: verum