:: deftheorem Def2 defines left-ideal IDEAL_1:def 2 :
for L being non empty multMagma
for F being Subset of L holds
( F is left-ideal iff for p, x being Element of L st x in F holds
p * x in F );