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