theorem Th55: :: FINSEQ_6:55

for D being non empty set
for p1, p2, p3 being Element of D st p1 <> p3 & p2 <> p3 holds
<*p1,p2,p3*> :- p3 = <*p3*>