let i1, i2 be natural Number ; ( ( i1 <= i2 or i1 <= i2 -' 1 ) implies ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) )
assume A1:
( i1 <= i2 or i1 <= i2 -' 1 )
; ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
A2:
now ( i1 <= i2 implies ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) )assume
i1 <= i2
;
( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )then A3:
i1 < i2 + 1
by NAT_1:13;
(i2 + 1) + 1
= i2 + (1 + 1)
;
hence
(
i1 < i2 + 1 &
i1 <= i2 + 1 &
i1 < (i2 + 1) + 1 &
i1 <= (i2 + 1) + 1 &
i1 < i2 + 2 &
i1 <= i2 + 2 )
by A3, NAT_1:13;
verum end;
now ( i1 <= i2 -' 1 implies ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) )end;
hence
( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
by A1, A2; verum