theorem Th4: :: FINSEQ_6:4

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