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