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

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 A4: ( 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 )
A5: dom F = {1,2} by A2, FINSEQ_1:4, FINSEQ_1:def 3;
A6: ( i in {1,2} & i + 1 in {1,2} ) by A2, A3, FINSEQ_1:4, FINSEQ_1:def 3;
A7: ( i = 1 or i = 2 ) by A3, A5, TARSKI:def 2;
commutators G1,((Omega). G) = {(1_ G)} by B1, GROUP_5:63;
then A8: [.G1,((Omega). G).] = gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:44
.= gr ({} the carrier of G) by XBOOLE_1:37
.= (1). G by GROUP_4:39 ;
( G1 = (Omega). G & G2 = (1). G ) by A1, FINSEQ_1:61, A4, A6, A7, 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 A4, A8, GROUP_2:77; :: 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 A2, Th25; :: thesis: verum