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