theorem :: TOPREALC:27

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V holds (v + u) - u = v