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;