let M be Cardinal; :: thesis: ( 0 in M iff 1 c= M )
0 + 1 = 1 ;
then nextcard (card 0 ) = card 1 by NAT_1:43;
hence ( 0 in M iff 1 c= M ) by Lm1, Th22; :: thesis: verum