theorem Th29: :: GROUP_9:29

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)