dom F is finite ;
then dom (max- F) is finite by Def11;
hence max- F is finite by FINSET_1:10; :: thesis: verum