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