theorem Th55: :: GROUP_9:55

for O being set
for G, H, I being GroupWithOperators of O st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic