:: deftheorem defines Permutations NUMBER17:def 2 :
for R being Relation holds Permutations R = { (p * R) where p is Permutation of (dom R) : verum } ;