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