IC SCM = NAT by AMI_2:30, FUNCT_7:def 1;
then ObjectKind (IC SCM ) = NAT by AMI_2:def 5;
hence ( SCM is IC-Ins-separated & SCM is definite ) by Th2, AMI_1:def 11; :: thesis: verum