n is Nat by TARSKI:1;
hence Seg n is n -element by Lm1, CARD_1:def 2; :: thesis: verum