( 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