theorem Th32: :: GROUP_9:32
for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 "\/" N2 is normal StableSubgroup of G