for i, j being Nat holds dl. i <> j ;