:: deftheorem Def10 defines permutational MATRIX_1:def 10 :
for IT being set holds
( IT is permutational iff ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n) );