theorem Th23: :: FINSEQ_6:23

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