consider x being strict Subspace of V;
x in Subspaces V by Def3;
hence not Subspaces V is empty ; :: thesis: verum