( ( i -' j = i - j & 0 <= i -' j ) or i -' j = 0 ) by XREAL_0:def 2;
hence i -' j is Element of NAT by INT_1:3; :: thesis: verum