theorem Th18: :: INT_7:18

for n being Nat st 1 < n holds
card (Segm0 n) = n - 1