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