for p being prime Nat
for G being finite Group
for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -group )