for G being Group
for H being strict Subgroup of G
for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds
g1 * g2 in (carr G) . H