theorem Th28: :: FINSEQ_6:28

for x, y, z being set st x <> z & y <> z holds
<*x,y,z*> -| z = <*x,y*>