theorem :: SEQM_3:42

for n, m, i, j being Nat holds
( |.(i - j).| + |.(n - m).| = 1 iff ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) )