let i, j be non empty 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:17;
hence i -' j < i by A1, XREAL_1:235; :: thesis: verum

end;

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

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

end;

end;