:: deftheorem Def1 defines SUBMODULE_DOMAIN LMOD_7:def 1 :
for K being Ring
for V being LeftMod of K
for b₃ being non empty set holds
( b₃ is SUBMODULE_DOMAIN of V iff for x being set st x in b₃ holds
x is strict Subspace of V );