:: deftheorem defines complementable ALGSTR_0:def 17 :
for M being addLoopStr holds
( M is complementable iff ( M is right_complementable & M is left_complementable ) );