theorem Th3: :: FINSEQ_6:3

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