theorem Th27: :: FINSEQ_6:27

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