card (Rev p) = card p by AFINSQ_2:def 1
.= n by CARD_1:def 7 ;
hence Rev p is n -element by CARD_1:def 7; :: thesis: verum