for G being Group
for g1, g2 being Element of G
for H being Subgroup of G st g1 in H & g2 in H holds
g1 * g2 in H