let i, j be natural number ; :: thesis: dl. i <> j
j in NAT by ORDINAL1:def 13;
hence dl. i <> j by ARYTM_3:38; :: thesis: verum