theorem Th77: :: MONOID_0:77

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