:: deftheorem defines left-invertible MONOID_0:def 3 :
for D being non empty set
for IT being BinOp of D holds
( IT is left-invertible iff for a, b being Element of D ex l being Element of D st IT . (l,a) = b );