set MySigmaField = {{},{1,2,3,4}};
set ThisSigma = bool {1,2,3,4};
{{},{1,2,3,4}} c= bool {1,2,3,4}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{},{1,2,3,4}} or x in bool {1,2,3,4} )
assume a1: x in {{},{1,2,3,4}} ; :: thesis: x in bool {1,2,3,4}
( x = {} or x = {1,2,3,4} ) by a1, TARSKI:def 2;
hence x in bool {1,2,3,4} by PROB_1:4, PROB_1:5; :: thesis: verum

end;

then reconsider MySigmaField = {{},{1,2,3,4}} as Subset-Family of {1,2,3,4} ;
A1: MySigmaField is compl-closed

proof

for A being Subset of {1,2,3,4} st A in MySigmaField holds
A ` in MySigmaField

proof

let A be Subset of {1,2,3,4}; :: thesis: ( A in MySigmaField implies A ` in MySigmaField )
assume A in MySigmaField ; :: thesis: A ` in MySigmaField

per cases then ( A = {} or A = {1,2,3,4} ) by TARSKI:def 2;

suppose A = {} ; :: thesis: A ` in MySigmaField

hence A ` in MySigmaField by TARSKI:def 2; :: thesis: verum

end;

suppose B1: A = {1,2,3,4} ; :: thesis: A ` in MySigmaField

A ` = {} by B1, XBOOLE_1:37;
hence A ` in MySigmaField by TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence MySigmaField is compl-closed ; :: thesis: verum

end;

MySigmaField is sigma-multiplicative

proof

for A1 being SetSequence of {1,2,3,4} st rng A1 c= MySigmaField holds
Intersection A1 in MySigmaField

proof

let A1 be SetSequence of {1,2,3,4}; :: thesis: ( rng A1 c= MySigmaField implies Intersection A1 in MySigmaField )
assume B1: rng A1 c= MySigmaField ; :: thesis: Intersection A1 in MySigmaField

per cases ( Intersection A1 = {} or Intersection A1 <> {} ) ;

suppose Intersection A1 = {} ; :: thesis: Intersection A1 in MySigmaField

hence Intersection A1 in MySigmaField by TARSKI:def 2; :: thesis: verum

end;

suppose Intersection A1 <> {} ; :: thesis: Intersection A1 in MySigmaField

hence Intersection A1 in MySigmaField by B1, Lm9; :: thesis: verum

end;

end;

end;

hence MySigmaField is sigma-multiplicative ; :: thesis: verum

end;

hence {{},{1,2,3,4}} is SigmaField of {1,2,3,4} by A1; :: thesis: verum