for n being Nat
for ITP being Element of Permutations n
for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "