theorem Th30: :: FINSEQ_6:30

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