IC SCMPDS = NAT by AMI_2:30, FUNCT_7:def 1;
then ObjectKind (IC SCMPDS ) = NAT by SCMPDS_1:def 4;
hence ( SCMPDS is IC-Ins-separated & SCMPDS is definite ) by Th3, AMI_1:def 11; :: thesis: verum