theorem :: AMI_3:10

for i, j being Nat st i <> j holds
dl. i <> dl. j by XTUPLE_0:1;