card (Seg n) = card n by Lm2;
hence card (Seg n) = n by CARD_1:def 2; :: according to CARD_1:def 7 :: thesis: verum