theorem Th5: :: FINSEQ_3:5

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