for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( M is sigma_finite iff ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ) by LM0902a, LM0902b;