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