a in nextcard a by CARD_1:32;
then omega c= nextcard a ;
hence not nextcard a is finite by CARD_3:102; :: thesis: verum