theorem :: GROUP_2:109

for G being Group
for H being Subgroup of G holds
( (1_ G) * H = carr H & H * (1_ G) = carr H ) by Th37;