theorem Th2: :: GOBRD10:2

for i1, i2 being Nat st i1,i2 are_adjacent & 1 <= i1 & 1 <= i2 holds
i1 -' 1,i2 -' 1 are_adjacent