Values (IC ) = NAT by FUNCT_7:def 1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by MEMSTR_0:def 6; :: thesis: verum