:: deftheorem defines are_adjacent GOBRD10:def 2 :
for i1, j1, i2, j2 being Nat holds
( i1,j1,i2,j2 are_adjacent iff ( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) ) );