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