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 Th64, 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 Th52;
then (i1 -' 1) + 1 <= i1 + 1 by XREAL_1:8;
then A2: (i1 -' 1) + 1 < i2 by A1, XXREAL_0:2;
((i1 -' 1) + 1) -' 1 <= (i1 -' 1) + 1 by Th52;
hence ( (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 ) by A2, XXREAL_0:2; :: thesis: ( i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
thus ( i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) by A1, Th64, NAT_1:13; :: thesis: verum