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