theorem Th38: :: GROUP_9:38

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds
H1 "\/" H3 is StableSubgroup of H2 "\/" H3