let A be set ; :: thesis: ( A is finite implies Fin A = bool A )
assume A1: A is finite ; :: thesis: Fin A = bool A
bool A c= Fin A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool A or x in Fin A )
assume A2: x in bool A ; :: thesis: x in Fin A
then x is finite by A1;
hence x in Fin A by A2, Def5; :: thesis: verum

end;

then ( bool A c= Fin A & Fin A c= bool A ) by Th26;
hence Fin A = bool A by XBOOLE_0:def 10; :: thesis: verum