let il be Instruction-Location of SCM+FSA ; :: thesis: for dl being Int-Location holds il <> dl
let dl be Int-Location ; :: thesis: il <> dl
( ObjectKind dl = INT & ObjectKind il = the Instructions of SCM+FSA ) by Th26, AMI_1:def 14;
hence il <> dl by SCMFSA_1:13; :: thesis: verum