theorem Th3: :: MESFUN16:3

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M is sigma_finite holds
COM M is sigma_finite