:: deftheorem defines lines LMOD_7:def 4 :
for K being Ring
for V being LeftMod of K
for b₃ being LINE_DOMAIN of V holds
( b₃ = lines V iff for x being object holds
( x in b₃ iff x is LINE of V ) );