now

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 consider W being strict Subspace of V such that
A1: W = x by VECTSP_5:def 3;
thus x is strict Subspace of V by A1; :: thesis: verum

end;

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