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