theorem Th4: :: MEASURE8:4

for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative