let i1, i2 be natural Number ; :: thesis: ( ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) implies ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) )
assume ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) ; :: thesis: ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
then (i1 + 1) + 1 <= i2 ;
hence A1: ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 ) by Th46, NAT_1:13; :: thesis: ( (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
i1 -' 1 <= i1 by Th35;
then (i1 -' 1) + 1 <= i1 + 1 by XREAL_1:6;
then A2: (i1 -' 1) + 1 < i2 by A1, XXREAL_0:2;
reconsider i1 = i1 as Nat by TARSKI:1;
((i1 -' 1) + 1) -' 1 <= (i1 -' 1) + 1 by Th35;
hence ( (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) by A1, Th46, A2, XXREAL_0:2, NAT_1:13; :: thesis: verum