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