:: deftheorem Def2 defines non-decreasing MEASURE2:def 2 :
for X being set
for S being SigmaField of X
for IT being N_Measure_fam of S holds
( IT is non-decreasing iff ex F being sequence of S st
( IT = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) ) );