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