theorem Th2: :: RING_1:2

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for b, c being Element of L holds c = b - (b - c)