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