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