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