theorem Th4: :: FINSEQ_3:4

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