:: deftheorem defines M2P PROB_4:def 2 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M . X = 1 holds
M2P M = M;