bool the carrier of A is finite ;
hence _bool A is finite by ThA10; :: thesis: verum