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