theorem :: LMOD_6:1

for x being set
for K being Ring
for M1, M2 being LeftMod of K st M1 = ModuleStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 ) ;