for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for x, y, z being Scalar of R holds
( ( x + y = z implies x = z - y ) & ( x = z - y implies x + y = z ) & ( x + y = z implies y = z - x ) & ( y = z - x implies x + y = z ) ) by Lm2, Lm3;