theorem Th33: :: FINSEQ_6:33

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