theorem Th8: :: GROUP_1:8

for G being Group holds (1_ G) " = 1_ G