let n be Nat; :: thesis: card (Seg n) = card n
Seg n,n are_equipotent by Lm1;
hence card (Seg n) = card n by CARD_1:5; :: thesis: verum