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 def3;
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:13;
then reconsider I = F . k as strict normal Subgroup of G by def2;
reconsider x = I /\ H as strict Subgroup of H ;
reconsider y = x as Element of the_normal_subgroups_of H by def2;
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;

A9: 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:5;
hence R . (len R) = (1). G by A1, A5, GROUP_2:103
.= (1). H by GROUP_2:75 ;
:: thesis: verum

end;

A10: 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 A11: ( 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 A12: ( 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
A13: ( I = F . i & R . i = I /\ H ) by A4, A11;
consider J being strict normal Subgroup of G such that
A14: ( J = F . (i + 1) & R . (i + 1) = J /\ H ) by A4, A11;
A15: ( i in dom F & i + 1 in dom F ) by A4, A11, FINSEQ_1:def 3;
then A16: J is strict normal Subgroup of I by A13, A14, A2, GROUP_6:9;
I ./. (I,J `*` ) is Subgroup of center (G ./. J) by A15, A13, A14, A2;
hence ( H2 is Subgroup of H1 & H1 ./. (H1,H2 `*` ) is Subgroup of center (H ./. H2) ) by A14, A16, A13, A12, Th26, 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, FINSEQ_1:def 3, A7, A9, A10; :: thesis: verum