for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing