let G be Group; :: thesis: ( G is nilpotent implies G is solvable )
assume G is nilpotent ; :: thesis: G is solvable
then 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 & ( 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) ) ) ) ;
reconsider R = F as FinSequence of Subgroups G by Th18;
A2: for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )

proof

let i be Element of NAT ; :: thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A3: ( i in dom R & i + 1 in dom R ) ; :: thesis: for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
then A4: ( F . i is strict normal Subgroup of G & F . (i + 1) is strict normal Subgroup of G ) by Th16;
let H1, H2 be Subgroup of G; :: thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A5: ( H1 = R . i & H2 = R . (i + 1) ) ; :: thesis: ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative

proof

let N be normal Subgroup of H1; :: thesis: ( N = H2 implies H1 ./. N is commutative )
assume A6: N = H2 ; :: thesis: H1 ./. N is commutative
then reconsider N9 = N as strict normal Subgroup of G by A5, A4;
A7: H1 ./. ((H1,N9) `*`) is Subgroup of center (G ./. N9) by A1, A3, A5, A6, A4;
center (G ./. N9) is commutative by GROUP_5:80;
hence H1 ./. N is commutative by A7, GROUP_6:def 1; :: thesis: verum

end;

hence ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) by A1, A3, A5, A4, GROUP_6:8; :: thesis: verum

end;

take R ; :: according to GRSOLV_1:def 1 :: thesis: ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b₁ being Element of NAT holds
( not b₁ in dom R or not K336(b₁,1) in dom R or for b₂, b₃ being Subgroup of G holds
( not b₂ = R . b₁ or not b₃ = R . K336(b₁,1) or ( b₃ is Subgroup of b₂ & ( for b₄ being Subgroup of b₂ holds
( not b₄ = b₃ or b₂ ./. b₄ is commutative ) ) ) ) ) ) )
thus ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b₁ being Element of NAT holds
( not b₁ in dom R or not K336(b₁,1) in dom R or for b₂, b₃ being Subgroup of G holds
( not b₂ = R . b₁ or not b₃ = R . K336(b₁,1) or ( b₃ is Subgroup of b₂ & ( for b₄ being Subgroup of b₂ holds
( not b₄ = b₃ or b₂ ./. b₄ is commutative ) ) ) ) ) ) ) by A1, A2; :: thesis: verum