theorem Th7: :: XTUPLE_0:7

for x, y being object
for X being set st [x,y] in X holds
y in union (union X)