theorem Th21: :: FINSEQ_6:21

for p1, p2, p3 being set holds p1 .. <*p1,p2,p3*> = 1