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