s
.
a
in
pi
(
(
product
(
(
SCM-VAL
R
)
*
SCM-OK
)
)
,
a
)
by
CARD_3:def 6
;
hence
s
.
a
is
Element
of
R
by
Th5
;
:: thesis:
verum