let G be Group; :: thesis: ( ex F being FinSequence of the_normal_subgroups_of G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) implies G is nilpotent )
given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and
A2: for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ; :: thesis: G is nilpotent
A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; :: thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
let H1, H2 be strict normal Subgroup of G; :: thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A5: ( H1 = F . i & H2 = F . (i + 1) ) ; :: thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
then H2 is strict Subgroup of H1 by A2, A4;
then A6: H1 ./. ((H1,H2) `*`) is Subgroup of G ./. H2 by GROUP_6:28;
G ./. H2 is commutative Group by A2, A4, A5;
hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) by A2, A4, A5, A6, GROUP_5:82; :: thesis: verum

end;

take F ; :: according to GRNILP_1:def 2 :: thesis: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) )
thus ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A1, A3; :: thesis: verum