let i1, i2 be Nat; :: thesis: ( i1,i2 are_adjacent & 1 <= i1 & 1 <= i2 implies i1 -' 1,i2 -' 1 are_adjacent )
assume that
A1: i1,i2 are_adjacent and
A2: 1 <= i1 and
A3: 1 <= i2 ; :: thesis: i1 -' 1,i2 -' 1 are_adjacent
0 <= i1 - 1 by A2, XREAL_1:48;
then A4: i1 -' 1 = i1 - 1 by XREAL_0:def 2;
0 <= i2 - 1 by A3, XREAL_1:48;
then A5: i2 -' 1 = i2 - 1 by XREAL_0:def 2;
( i2 = i1 + 1 or i1 = i2 + 1 ) by A1;
then ( i2 - 1 = (i1 - 1) + 1 or i1 - 1 = (i2 - 1) + 1 ) ;
hence i1 -' 1,i2 -' 1 are_adjacent by A4, A5; :: thesis: verum