theorem Th91: :: GROUP_9:91

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