not the
carrier
of
R
\/
the
carrier
of
S
is
empty
;
hence
not
sum_of
(
R
,
S
) is
empty
by
NECKLA_2:def 3
;
:: thesis:
verum