:: deftheorem Def2 defines nilpotent GRNILP_1:def 2 :
for IT being Group holds
( IT is nilpotent iff ex F being FinSequence of the_normal_subgroups_of IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( 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 IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ) );