:: deftheorem Def3 defines LINE_DOMAIN LMOD_7:def 3 :
for K being Ring
for V being LeftMod of K
for b₃ being non empty set holds
( b₃ is LINE_DOMAIN of V iff for x being set st x in b₃ holds
x is LINE of V );