set x = the strict Subspace of V;
the strict Subspace of V in Subspaces V by Def3;
hence not Subspaces V is empty ; :: thesis: verum