for n being Nat holds
( n > 0 iff Seg n <> {} ) ;