theorem Th92: :: GROUP_9:92

for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)