let k be Nat; :: thesis: card (k \/ {k}) = k + 1
not k in k ;
then card (k \/ {k}) = (card k) + 1 by CARD_2:41
.= k + 1 ;
hence card (k \/ {k}) = k + 1 ; :: thesis: verum