set MyOmega = {{},{1,2},{3,4},{1,2,3,4}};
{{},{1,2},{3,4},{1,2,3,4}} is Subset-Family of {1,2,3,4}
proof
for x being object st x in {{},{1,2},{3,4},{1,2,3,4}} holds
x in bool {1,2,3,4}
proof
let x be object ; :: thesis: ( x in {{},{1,2},{3,4},{1,2,3,4}} implies x in bool {1,2,3,4} )
assume x in {{},{1,2},{3,4},{1,2,3,4}} ; :: thesis: x in bool {1,2,3,4}
per cases then ( x = {} or x = {1,2} or x = {3,4} or x = {1,2,3,4} ) by ENUMSET1:def 2;
suppose x = {} ; :: thesis: x in bool {1,2,3,4}
hence x in bool {1,2,3,4} by PROB_1:4; :: thesis: verum
end;
suppose x = {1,2} ; :: thesis: x in bool {1,2,3,4}
hence x in bool {1,2,3,4} by Lm2; :: thesis: verum
end;
suppose x = {3,4} ; :: thesis: x in bool {1,2,3,4}
hence x in bool {1,2,3,4} by Lm1; :: thesis: verum
end;
suppose x = {1,2,3,4} ; :: thesis: x in bool {1,2,3,4}
hence x in bool {1,2,3,4} by ZFMISC_1:def 1; :: thesis: verum
end;
end;
end;
hence {{},{1,2},{3,4},{1,2,3,4}} is Subset-Family of {1,2,3,4} by TARSKI:def 3; :: thesis: verum
end;
then reconsider MyOmega = {{},{1,2},{3,4},{1,2,3,4}} as Subset-Family of {1,2,3,4} ;
A1: MyOmega is compl-closed
proof
for A being Subset of {1,2,3,4} st A in MyOmega holds
A ` in MyOmega
proof
let A be Subset of {1,2,3,4}; :: thesis: ( A in MyOmega implies A ` in MyOmega )
assume A in MyOmega ; :: thesis: A ` in MyOmega
per cases then ( A = {} or A = {1,2} or A = {3,4} or A = {1,2,3,4} ) by ENUMSET1:def 2;
suppose A = {} ; :: thesis: A ` in MyOmega
hence A ` in MyOmega by ENUMSET1:def 2; :: thesis: verum
end;
suppose A = {1,2} ; :: thesis: A ` in MyOmega
hence A ` in MyOmega by Lem1, ENUMSET1:def 2; :: thesis: verum
end;
suppose A = {3,4} ; :: thesis: A ` in MyOmega
hence A ` in MyOmega by Lem2, ENUMSET1:def 2; :: thesis: verum
end;
suppose B300: A = {1,2,3,4} ; :: thesis: A ` in MyOmega
A ` = {}
proof
reconsider B = {} as Subset of {1,2,3,4} by SUBSET_1:1;
A = B ` by B300;
hence A ` = {} ; :: thesis: verum
end;
hence A ` in MyOmega by ENUMSET1:def 2; :: thesis: verum
end;
end;
end;
hence MyOmega is compl-closed ; :: thesis: verum
end;
MyOmega is sigma-multiplicative by Lm8;
hence {{},{1,2},{3,4},{1,2,3,4}} is SigmaField of {1,2,3,4} by A1; :: thesis: verum