for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y being Element of R ex z being Element of R st
( x = y + z & x = z + y )