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