theorem Th1: :: FINSEQ_3:1

Seg 3 = {1,2,3}