theorem Th5: :: FINSEQ_6:5

for p1, p2, p3 being set holds <*p1,p2,p3*> | (Seg 2) = <*p1,p2*>