theorem :: SCMRING2:8

for R being Ring holds IC = NAT by Def1;