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