theorem Th13: :: XTUPLE_0:13

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