let i be Element of NAT ; :: thesis: IC <> dl. i
assume IC = dl. i ; :: thesis: contradiction
then NAT = [1,i] by Th1, AMI_3:def 11;
hence contradiction ; :: thesis: verum