theorem Th34: :: FINSEQ_6:34

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