now :: thesis: for x being set st x in Submodules V holds

x is strict Subspace of V

hence
Subspaces V is SUBMODULE_DOMAIN of V
by Def1; :: thesis: verumx 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;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