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