for X1, X2, X3 being non empty set holds { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P₁[x1,x2,x3] } is Subset of [:X1,X2,X3:]