:: deftheorem Def15 defines left_complementable ALGSTR_0:def 15 :
for M being addLoopStr holds
( M is left_complementable iff for x being Element of M holds x is left_complementable );