theorem :: FINSEQ_3:6

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