:: deftheorem defines are_adjacent GOBRD10:def 1 :
for i1, i2 being Nat holds
( i1,i2 are_adjacent iff ( i2 = i1 + 1 or i1 = i2 + 1 ) );