:: deftheorem Def16 defines right_complementable ALGSTR_0:def 16 :
for M being addLoopStr holds
( M is right_complementable iff for x being Element of M holds x is right_complementable );