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