A1: rng F is N_Sub_set_fam of X by MEASURE1:52;
rng F c= S by RELAT_1:def 19;
hence rng F is N_Measure_fam of S by A1, MEASURE2:def 1; :: thesis: verum