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