reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;
5 in {1,2,3,4,5} by ENUMSET1:def 3;
then [5,{},<*mk,ml*>] in SCM-Instr by SCM_INST:4;
hence [5,{},<*a,b*>] is Instruction of SCM ; :: thesis: verum