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