theorem :: MEASURE1:34

for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds
( {} in S & X in S & ( for A, B being set st A in S & B in S holds
( X \ A in S & A \/ B in S & A /\ B in S ) ) ) by Def1, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1:4, PROB_1:5;