:: deftheorem defines -placesOf FOMODEL3:def 6 :
for X being non empty set
for R being Relation of X
for n being Nat holds n -placesOf R = n -placesOf R;