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