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