:: deftheorem defines -placesOf FOMODEL3:def 5 :
for X, Y being non empty set
for R being Relation of X,Y
for n being Nat holds n -placesOf R = { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } ;