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