for x being set
for G being Group holds
( x in (1). G iff x = 1_ G )