let G be Group; ( G is nilpotent implies G is solvable )
assume
G is nilpotent
; 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 ) )
take
R
; GRSOLV_1:def 1 ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds
( not b1 in dom R or not K336(b1,1) in dom R or for b2, b3 being Subgroup of G holds
( not b2 = R . b1 or not b3 = R . K336(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds
( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) )
thus
( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds
( not b1 in dom R or not K336(b1,1) in dom R or for b2, b3 being Subgroup of G holds
( not b2 = R . b1 or not b3 = R . K336(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds
( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) )
by A1, A2; verum