theorem Th3: :: FINSEQ_1:3

for a being natural Number holds
( a = 0 or a in Seg a )