for x, X being set holds
( x is Element of (GPerms X) iff x is Permutation of X )