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;