theorem Th22: :: FINSEQ_6:22

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