A2: {{1,2,3,4}} c= bool {1,2,3,4} by ZFMISC_1:68;
{{},{1,2},{3,4},{1,2,3,4}} c= bool {1,2,3,4}

proof

set MyBool = bool {1,2,3,4};
reconsider MyBool = bool {1,2,3,4} as SigmaField of {1,2,3,4} ;
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 B25; :: thesis: verum

end;

suppose x = {3,4} ; :: thesis: x in bool {1,2,3,4}

hence x in bool {1,2,3,4} by B26; :: thesis: verum

end;

suppose x = {1,2,3,4} ; :: thesis: x in bool {1,2,3,4}

then x in {{1,2,3,4}} by TARSKI:def 1;
hence x in bool {1,2,3,4} by A2; :: thesis: verum

end;

end;

end;

hence {{},{1,2},{3,4},{1,2,3,4}} c= bool {1,2,3,4} ; :: thesis: verum

end;

hence {{},{1,2},{3,4},{1,2,3,4}} c< bool {1,2,3,4} by The0; :: thesis: verum