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