theorem Th1: :: RING_1:1

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