dom (F | A) c= A by RELAT_1:58;
hence F | A is finite by Th29; :: thesis: verum