theorem Th58: :: GROUP_9:58

for O being set
for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is trivial holds
H is trivial