let A be set ; :: thesis: ( A is finite implies Fin A = bool A )
assume A1: A is finite ; :: thesis: Fin A = bool A
A2: 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 x in bool A ; :: thesis: x in Fin A
hence x in Fin A by A1, Def5; :: thesis: verum

end;

Fin A c= bool A by Th26;
hence Fin A = bool A by A2, XBOOLE_0:def 10; :: thesis: verum