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