theorem Th2: :: FINSEQ_3:2

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