for R being Ring holds IC = NAT by Def1;