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