theorem :: MEASURE1:27

for X being set
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = 0. ) & ( A <> {} implies M . A = +infty ) ) by Th26;