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 ;
TARSKI:def 3 ( not x in {{},{1,2,3,4}} or x in bool {1,2,3,4} )
assume a1:
x in {{},{1,2,3,4}}
;
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;
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};
( A in MySigmaField implies A ` in MySigmaField )
assume
A in MySigmaField
;
A ` in MySigmaField
end;
hence
MySigmaField is
compl-closed
;
verum
end;
MySigmaField is sigma-multiplicative
hence
{{},{1,2,3,4}} is SigmaField of {1,2,3,4}
by A1; verum