(
rng
F
is
N_Sub_set_fam
of
X
&
rng
F
c=
S
)
by
MEASURE1:23
,
RELAT_1:def 19
;
hence
rng
F
is
N_Measure_fam
of
S
by
MEASURE2:def 1
;
:: thesis:
verum