theorem Th20: :: FINSEQ_6:20

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