theorem :: GROUP_22:70

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 & K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H holds
K is characteristic Subgroup of G