for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )