card (n --> k) = n ;
hence n --> k is n -element by CARD_1:def 7; :: thesis: verum