theorem Th3: :: RLVECT_1:3

for V being right_complementable add-associative right_zeroed addLoopStr holds V is right_add-cancelable