let G be Group; ( 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)
; 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 ;
( 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 )
;
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;
( 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) )
;
( 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;
verum
end;
hence
G is nilpotent
by A1, Th21; verum