theorem Th1: :: GROUP_5:1

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