let j be Element of NAT ; :: thesis: (j -' j) + 1 = 1
j -' j = j - j by XREAL_1:233
.= 0 ;
hence (j -' j) + 1 = 1 ; :: thesis: verum