let n be natural number ; :: thesis: ( 1 < n implies card (Segm0 n) = n - 1 )
A1: card (Segm n) = n by CARD_1:def 2;
assume A2: 1 < n ; :: thesis: card (Segm0 n) = n - 1
then A3: 0 in Segm n by NAT_1:44;
A4: card {0} = 1 by CARD_1:30;
Segm0 n = (Segm n) \ {0} by A2, Def2;
hence card (Segm0 n) = n - 1 by A1, A3, A4, EULER_1:4; :: thesis: verum