theorem :: GROUP_2:77

for G being Group
for H being Subgroup of G holds (carr H) " = carr H