A1: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;
IC = NAT by Def1;
then Values (IC ) = NAT by A1, SCMRING1:2;
hence SCM R is IC-Ins-separated ; :: thesis: verum