theorem Th82: :: GROUP_9:82

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