IC = NAT by AMI_2:22, FUNCT_7:def 1;
then ObjectKind (IC ) = NAT by SCMPDS_1:def 2;
hence SCMPDS is IC-Ins-separated by MEMSTR_0:def 3; :: thesis: verum