the carrier of (Group_of_Perm n) = Permutations n by Def6;
hence not the carrier of (Group_of_Perm n) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum