consider r being Nat such that
A1: card G = p |^ r by GROUP_10:def 17;
A2: card G = (card N) * (index N) by GROUP_2:147;
A3: card (G ./. N) = index N by GROUP_6:27;
reconsider n = card (G ./. N) as Nat ;
n divides p |^ r by A1, A2, A3, NAT_D:def 3;
then ex r1 being Nat st
( n = p |^ r1 & r1 <= r ) by Th2;
hence G ./. N is p -group ; :: thesis: verum