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