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