theorem Th78: :: GROUP_24:74

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