2 in {1,2,3,4} by ENUMSET1:def 2;
then [2,<*a,b*>] in SCM-Instr R by Th4;
hence [2,<*a,b*>] is Instruction of by Def1; :: thesis: verum