IC = NAT by AMI_2:22, FUNCT_7:def 1;
then Values (IC ) = NAT by AMI_2:6;
hence SCM is IC-Ins-separated by MEMSTR_0:def 6; :: thesis: verum