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

now

let x be set ; :: 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 Th10;
hence x in bool A ; :: thesis: verum

end;

hence TWOELEMENTSETS A c= bool A by TARSKI:def 3; :: thesis: verum