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