for O being set
for G being strict GroupWithOperators of O st G is trivial holds
(1). G = G