for X being set
for S being Field_Subset of X
for M being 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;