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