let G be Group; :: thesis: ( G is commutative implies G is nilpotent )
assume A1: G is commutative ; :: thesis: G is nilpotent
( (Omega). G in the_normal_subgroups_of G & (1). G in the_normal_subgroups_of G ) by Def1;
then <*((Omega). G),((1). G)*> is FinSequence of the_normal_subgroups_of G by FINSEQ_2:13;
then consider F being FinSequence of the_normal_subgroups_of G such that
A2: F = <*((Omega). G),((1). G)*> ;
A3: ( len F = 2 & F . 1 = (Omega). G & F . 2 = (1). G ) by A2, FINSEQ_1:44;
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,((Omega). G).] is Subgroup of G2 )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; :: thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 )

now :: thesis: for G1, G2 being Subgroup of G st G1 = F . i & G2 = F . (i + 1) 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,((Omega). G).] is Subgroup of G2 )

let G1, G2 be Subgroup of G; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) )
assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 )
A6: dom F = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def 3;
A7: ( i in {1,2} & i + 1 in {1,2} ) by A3, A4, FINSEQ_1:2, FINSEQ_1:def 3;
A8: ( i = 1 or i = 2 ) by A4, A6, TARSKI:def 2;
commutators (G1,((Omega). G)) = {(1_ G)} by A1, GROUP_5:57;
then A9: [.G1,((Omega). G).] = gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35
.= gr ({} the carrier of G) by XBOOLE_1:37
.= (1). G by GROUP_4:30 ;
( G1 = (Omega). G & G2 = (1). G ) by A2, A5, A7, A8, TARSKI:def 2;
hence for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) by A5, A9, GROUP_2:65; :: thesis: verum

end;

hence for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ; :: thesis: verum

end;

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