theorem Th7: :: FINSEQ_3:7

for k being Nat holds
( Seg k = {} iff not k in Seg k )