not dom f is trivial ;
then not dom (Card f) is trivial by CARD_3:def 2;
hence not Card f is trivial ; :: thesis: verum