theorem GROUP252INV: :: GROUP_18:9

for G, H being Group
for K being Subgroup of H
for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K