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