let dl be Int-Location ; :: thesis: dl <> IC SCM+FSA
( ObjectKind dl = INT & ObjectKind (IC SCM+FSA ) = NAT ) by Th26, AMI_1:def 11;
hence dl <> IC SCM+FSA by SCMFSA_1:13; :: thesis: verum