:: deftheorem defines left_complementable ALGSTR_0:def 10 :
for M being addLoopStr
for x being Element of M holds
( x is left_complementable iff ex y being Element of M st y + x = 0. M );