let i, i1 be natural Number ; :: thesis: ( ( i -' i1 >= 1 or i - i1 >= 1 ) implies i -' i1 = i - i1 )
assume A1: ( i -' i1 >= 1 or i - i1 >= 1 ) ; :: thesis: i -' i1 = i - i1
per cases ( i -' i1 >= 1 or i - i1 >= 1 ) by A1;
suppose i -' i1 >= 1 ; :: thesis: i -' i1 = i - i1
hence i -' i1 = i - i1 by XREAL_0:def 2; :: thesis: verum
end;
suppose i - i1 >= 1 ; :: thesis: i -' i1 = i - i1
hence i -' i1 = i - i1 by XREAL_0:def 2; :: thesis: verum
end;
end;