let G be strict commutative Group; :: thesis: G is solvable
( (Omega). G in Subgroups G & (1). G in Subgroups G ) by GROUP_3:def 1;
then <*((Omega). G),((1). G)*> is FinSequence of Subgroups G by FINSEQ_2:13;
then consider F being FinSequence of Subgroups G such that
A1: F = <*((Omega). G),((1). G)*> ;
A2: F . 1 = (Omega). G by A1;
A3: len F = 2 by A1, FINSEQ_1:44;
A4: F . 2 = (1). G by A1;
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume that
A5: i in dom F and
A6: i + 1 in dom F ; :: thesis: for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )

now :: thesis: for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )

let G1, G2 be strict Subgroup of G; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume A7: ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
dom F = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def 3;
then A8: ( i = 1 or i = 2 ) by A5, TARSKI:def 2;
A9: i + 1 in {1,2} by A3, A6, FINSEQ_1:2, FINSEQ_1:def 3;
for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative by A2, A4, A7, A9, A8, GROUP_6:71, GROUP_6:77, TARSKI:def 2;
hence ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) by A1, A7, A9, A8, TARSKI:def 2; :: thesis: verum

end;

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

end;

hence G is solvable by A3, A2, A4; :: thesis: verum