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 being strict normal Subgroup of G st G1 = F . i holds
[.G1,((Omega). G).] = F . (i + 1) ) ) 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 being strict normal Subgroup of G st G1 = F . i holds
[.G1,((Omega). G).] = F . (i + 1) ; :: thesis: G is nilpotent
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 Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of 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 Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) )
assume A3: ( 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 Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 )
let H1, H2 be strict normal Subgroup of G; :: thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) )
assume ( H1 = F . i & H2 = F . (i + 1) ) ; :: thesis: ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 )
then H2 = [.H1,((Omega). G).] by A2, A3;
hence ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) by Th15, GROUP_2:54; :: thesis: verum

end;

hence G is nilpotent by A1, Th21; :: thesis: verum