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