let n be Nat; :: thesis: card n = n
card n = card (card n) ;
hence card n = n by CARD_1:71; :: thesis: verum