theorem :: FINTOPO5:2

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