:: deftheorem defines "\/" GROUP_9:def 27 :
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of ((carr H1) \/ (carr H2));