theorem Th21: :: XTUPLE_0:21

for x, x1, x2, x3 being object
for X being set st [x1,x,x2,x3] in X holds
x in proj2_4 X