let i be Nat; :: thesis: ( IC <> dl. i & IC <> i )
thus IC <> dl. i by Th1; :: thesis: IC <> i
assume IC = i ; :: thesis: contradiction
then IC in NAT by ORDINAL1:def 12;
hence contradiction by Th1; :: thesis: verum