theorem Th77: :: GROUP_24:73

for G being Group holds
( G is trivial iff for x being Element of G holds x = 1_ G )