let i be natural number ; :: thesis: ( IC <> dl. i & IC <> i )
thus IC <> dl. i by Th4, ARYTM_3:30; :: thesis: IC <> i
assume IC = i ; :: thesis: contradiction
then IC in NAT by ORDINAL1:def 12;
hence contradiction by Th4; :: thesis: verum