dom F is empty ;
then dom (Card F) is empty by CARD_3:def 2;
hence Card F is empty ; :: thesis: verum