for A being set holds
( A in COM Sigma,P iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by Def5;
hence COM Sigma,P is SigmaField of Omega by Th35; :: thesis: verum