theorem :: GRNILP_1:27

for G being Group st 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) ) ) holds
G is nilpotent