let i, i1 be natural Number ; :: thesis: ( ( i -' i1 >= 1 or i - i1 >= 1 ) implies (i -' i1) + i1 = i )
assume ( i -' i1 >= 1 or i - i1 >= 1 ) ; :: thesis: (i -' i1) + i1 = i
then (i -' i1) + i1 = (i - i1) + i1 by Th39
.= i ;
hence (i -' i1) + i1 = i ; :: thesis: verum