theorem :: GROUP_4:50

for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2)