theorem :: LMOD_6:9

for x being set
for K being Ring
for V being LeftMod of K holds
( x in [#] V iff x in V ) ;