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