let M be Cardinal; :: thesis: ( 0 in M iff 1 c= M )
0 + 1 = 1 ;
then nextcard (card 0) = card 1 by NAT_1:42;
hence ( 0 in M iff 1 c= M ) by Lm3, CARD_3:90; :: thesis: verum