let i be Element of NAT ; :: thesis: ( IC <> dl. i & IC <> i )

hereby :: thesis: IC <> i

assume IC = dl. i ; :: thesis: contradiction
then NAT = [1,i] by Th6, AMI_3:def 11;
hence contradiction by ARYTM_3:30; :: thesis: verum

end;

assume IC = i ; :: thesis: contradiction
then NAT = i by Th6;
then NAT in NAT ;
hence contradiction ; :: thesis: verum