let n be Nat; :: thesis: permutations (Seg n) = Permutations n
thus permutations (Seg n) c= Permutations n :: according to XBOOLE_0:def 10 :: thesis: Permutations n c= permutations (Seg n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in permutations (Seg n) or x in Permutations n )
assume x in permutations (Seg n) ; :: thesis: x in Permutations n
then x is Permutation of (Seg n) by Th1;
hence x in Permutations n by MATRIX_1:def 12; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in permutations (Seg n) )
assume x in Permutations n ; :: thesis: x in permutations (Seg n)
then x is Permutation of (Seg n) by MATRIX_1:def 12;
hence x in permutations (Seg n) ; :: thesis: verum