for K being disjoint_valued Function of NAT,Family_of_Intervals st Union K in Family_of_Intervals holds
pre-Meas . (Union K) <= SUM (pre-Meas * K)