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