let x be set ; :: according to MONOID_0:def 1 :: thesis: ( x is Element of the carrier of (Group_of_Perm n) implies x is set )

the carrier of (Group_of_Perm n) = Permutations n by MATRIX_1:def 13;

hence ( x is Element of the carrier of (Group_of_Perm n) implies x is set ) ; :: thesis: verum

the carrier of (Group_of_Perm n) = Permutations n by MATRIX_1:def 13;

hence ( x is Element of the carrier of (Group_of_Perm n) implies x is set ) ; :: thesis: verum