A |` F c= F by RELAT_1:86;
hence A |` F is finite ; :: thesis: verum