theorem Th16: :: MIDSP_2:16

for G being non empty right_complementable Fanoian add-associative right_zeroed addLoopStr
for x being Element of G st x = - x holds
x = 0. G