theorem Th7: :: MODCAT_1:7

for UN being Universe
for R being Ring
for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R