theorem Th26: :: FINSEQ_6:26

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