theorem Th3: :: RING_1:3

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