theorem Th3: :: FINSEQ_3:3

Seg 5 = {1,2,3,4,5}