theorem :: GROUP_22:69

for G being finite Group
for H being strict characteristic Subgroup of G
for K being strict Subgroup of G st H is Subgroup of K holds
H is normal Subgroup of K