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