let i, j be natural Number ; :: thesis: (i + j) -' j = i
(i + j) - j >= 0 ;
hence (i + j) -' j = i by XREAL_0:def 2; :: thesis: verum