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 JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
(H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic