:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :
for R being Ring
for b₂ being non empty set holds
( b₂ is LeftMod_DOMAIN of R iff for x being Element of b₂ holds x is strict LeftMod of R );