thus N_Real is right_complementable :: thesis: N_Real is right_add-cancelable
proof
let a be Element of N_Real; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider b = - a as Element of N_Real by XREAL_0:def 1;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. N_Real
thus a + b = 0. N_Real ; :: thesis: verum
end;
let a be Element of N_Real; :: according to ALGSTR_0:def 7 :: thesis: a is right_add-cancelable
thus for b, c being Element of N_Real st b + a = c + a holds
b = c ; :: according to ALGSTR_0:def 4 :: thesis: verum