:: deftheorem defines "\/" GROUP_4:def 9 :
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2));