theorem :: GROUP_24:13

for G being Group
for H, K being Subgroup of G
for HK being Subgroup of K st multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of HK, the multF of HK #) holds
carr H = carr HK ;