let A be set ; :: thesis: TWOELEMENTSETS A c= bool A

now :: thesis: for x being object st x in TWOELEMENTSETS A holds
x in bool A

let x be object ; :: thesis: ( x in TWOELEMENTSETS A implies x in bool A )
assume x in TWOELEMENTSETS A ; :: thesis: x in bool A
then x is finite Subset of A by Th8;
hence x in bool A ; :: thesis: verum

end;

hence TWOELEMENTSETS A c= bool A ; :: thesis: verum