theorem Th8: :: GROUP_1:8
for G being Group holds (1_ G) " = 1_ G