theorem Th15: :: XTUPLE_0:15

for x, y, z being object
for X being set st [x,y,z] in X holds
y in proj2_3 X