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;
(i1 -' 1) -' 1 <= i1 -' 1 by Th35;
hence i1 -' 2 < i2 by A3, A4, XXREAL_0:2; :: thesis: i1 <= i2
thus i1 <= i2 by A1, NAT_1:13; :: thesis: verum