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