given N being Cardinal such that A1: omega = nextcard N ; :: according to CARD_1:def 4 :: thesis: contradiction
N in omega by A1, Th17;
then A2: succ N in omega by ORDINAL1:def 12;
reconsider n = N as Element of omega by A1, Th17;
( nextcard (card n) = card (succ n) & card n = n ) by Th42;
hence contradiction by A1, A2; :: thesis: verum