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