let A be set ; :: thesis: TWOELEMENTSETS A c= bool A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TWOELEMENTSETS A or 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