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 Lm3, Th107; :: thesis: verum