now :: thesis: for x being set st x in Submodules V holds
x is strict Subspace of V

let x be set ; :: thesis: ( x in Submodules V implies x is strict Subspace of V )
assume x in Submodules V ; :: thesis: x is strict Subspace of V
then ex W being strict Subspace of V st W = x by VECTSP_5:def 3;
hence x is strict Subspace of V ; :: thesis: verum

end;

hence Subspaces V is SUBMODULE_DOMAIN of V by Def1; :: thesis: verum