:: deftheorem Def5 defines Permutations MATRIX_1:def 12 :
for n being Nat
for b₂ being set holds
( b₂ = Permutations n iff for x being set holds
( x in b₂ iff x is Permutation of (Seg n) ) );