let H be Subgroup of G; :: thesis: H is nilpotent
consider 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 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2;
defpred S₁[ set , set ] means ex I being strict normal Subgroup of G st
( I = F . G & c₂ = I /\ H );
A3: for k being Nat st k in Seg (len F) holds
ex x being Element of the_normal_subgroups_of H st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of H st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of the_normal_subgroups_of H st S₁[k,x]
then k in dom F by FINSEQ_1:def 3;
then F . k in the_normal_subgroups_of G by FINSEQ_2:11;
then reconsider I = F . k as strict normal Subgroup of G by Def1;
reconsider x = I /\ H as strict Subgroup of H ;
reconsider y = x as Element of the_normal_subgroups_of H by Def1;
take y ; :: thesis: S₁[k,y]
take I ; :: thesis: ( I = F . k & y = I /\ H )
thus ( I = F . k & y = I /\ H ) ; :: thesis: verum

end;

consider R being FinSequence of the_normal_subgroups_of H such that
A4: ( dom R = Seg (len F) & ( for i being Nat st i in Seg (len F) holds
S₁[i,R . i] ) ) from FINSEQ_1:sch 5(A3);
A5: len R = len F by A4, FINSEQ_1:def 3;
A6: len R > 0 by A1, A4, FINSEQ_1:def 3;
A7: R . 1 = (Omega). H

proof

1 <= len R by A6, NAT_1:14;
then 1 in Seg (len F) by A5;
then ex I being strict normal Subgroup of G st
( I = F . 1 & R . 1 = I /\ H ) by A4;
hence R . 1 = (Omega). H by A1, Lm4; :: thesis: verum

end;

A8: R . (len R) = (1). H

proof

ex I being strict normal Subgroup of G st
( I = F . (len R) & R . (len R) = I /\ H ) by A1, A4, A5, FINSEQ_1:3;
hence R . (len R) = (1). G by A1, A5, GROUP_2:85
.= (1). H by GROUP_2:63 ;
:: thesis: verum

end;

A9: for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )

proof

let i be Element of NAT ; :: thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) )
assume A10: ( i in dom R & i + 1 in dom R ) ; :: thesis: for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
let H1, H2 be strict normal Subgroup of H; :: thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) )
assume A11: ( H1 = R . i & H2 = R . (i + 1) ) ; :: thesis: ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
consider I being strict normal Subgroup of G such that
A12: ( I = F . i & R . i = I /\ H ) by A4, A10;
consider J being strict normal Subgroup of G such that
A13: ( J = F . (i + 1) & R . (i + 1) = J /\ H ) by A4, A10;
A14: ( i in dom F & i + 1 in dom F ) by A4, A10, FINSEQ_1:def 3;
then A15: J is strict normal Subgroup of I by A12, A13, A2, GROUP_6:8;
I ./. ((I,J) `*`) is Subgroup of center (G ./. J) by A14, A12, A13, A2;
hence ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) by A13, A15, A12, A11, Th22, Lm5; :: thesis: verum

end;

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