theorem :: LMOD_7:8

for K being Ring
for V being LeftMod of K holds
( SubMeet V is commutative & SubMeet V is associative & SubMeet V is having_a_unity & (Omega). V = the_unity_wrt (SubMeet V) )