set IT = OS_Meas | Family_of_Intervals;
A1: ( OS_Meas is nonnegative & OS_Meas is zeroed ) by MEASURE4:def 1;
reconsider IT = OS_Meas | Family_of_Intervals as Function of Family_of_Intervals,ExtREAL by FUNCT_2:32;
A2: dom IT = Family_of_Intervals by FUNCT_2:def 1;

A3: now :: thesis: for x being Element of Family_of_Intervals holds IT . x >= 0

let x be Element of Family_of_Intervals ; :: thesis: IT . x >= 0
IT . x = OS_Meas . x by A2, FUNCT_1:47;
hence IT . x >= 0 by A1, MEASURE1:def 2; :: thesis: verum

end;

IT . {} = OS_Meas . {} by A2, SETFAM_1:def 8, FUNCT_1:47;
then IT . {} = 0 by A1, VALUED_0:def 19;
hence OS_Meas | Family_of_Intervals is zeroed nonnegative Function of Family_of_Intervals,ExtREAL by A3, VALUED_0:def 19, MEASURE1:def 2; :: thesis: verum