reconsider a = a as Element of SCM-Data-Loc by Def2;
reconsider loc = loc as Element of NAT by ORDINAL1:def 12;
7 in {7,8} by TARSKI:def 2;
then [7,<*loc*>,<*a*>] in SCM-Instr by AMI_2:3;
hence [7,<*loc*>,<*a*>] is Instruction of SCM ; :: thesis: verum