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 by A1, Def5;
Fin A c= bool A by Th13;
hence Fin A = bool A by A2; :: thesis: verum