theorem :: GROUPP_1:31

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