:: deftheorem defines -tuple2Class FOMODEL3:def 14 :
for U being non empty set
for n being Nat
for E being Equivalence_Relation of U holds n -tuple2Class E = (n -placesOf ((E -class) ~)) * ((n -placesOf E) -class);