theorem :: AMI_3:12

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