:: deftheorem defines complementable ALGSTR_0:def 12 :
for M being addLoopStr
for x being Element of M holds
( x is complementable iff ( x is right_complementable & x is left_complementable ) );