theorem Th57: :: GROUP_9:57

for O being set
for G being strict GroupWithOperators of O holds G ./. ((Omega). G) is trivial