:: deftheorem defines c= LMOD_6:def 5 :
for K being Ring
for M, N being LeftMod of K holds
( M c= N iff M is Subspace of N );