let A be set ; :: thesis: Fin A c= bool A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fin A or x in bool A )
assume x in Fin A ; :: thesis: x in bool A
then x c= A by Def5;
hence x in bool A ; :: thesis: verum