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