let i, j be non zero Nat; :: thesis: i -' j < i

per cases ( j <= i or j > i ) ;

suppose A1: j <= i ; :: thesis: i -' j < i

i - j < i - 0 by XREAL_1:15;
hence i -' j < i by A1, XREAL_1:233; :: thesis: verum

end;

suppose j > i ; :: thesis: i -' j < i

hence i -' j < i by Th8; :: thesis: verum

end;

end;