let i1, i2, j1, j2 be Element of NAT ; :: thesis: ( i1,j1,i2,j2 are_adjacent2 & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 implies i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2 )
assume that
A1: i1,j1,i2,j2 are_adjacent2 and
A2: ( 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 ) ; :: thesis: i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2
( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) by A1, Def2;
then ( ( i1 -' 1,i2 -' 1 are_adjacent1 & j1 -' 1 = j2 -' 1 ) or ( i1 -' 1 = i2 -' 1 & j1 -' 1,j2 -' 1 are_adjacent1 ) ) by A2, Th2;
hence i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2 by Def2; :: thesis: verum