theorem Th12: :: LATSUBGR:12
for G being Group
for A being Subset of G st A = {(1_ G)} holds
gr A = (1). G