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:15;
then consider F being FinSequence of Subgroups 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 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 A3: ( i in dom F & 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

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 A4: ( 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 ) )
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;
for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative

proof

let N be normal Subgroup of G1; :: thesis: ( N = G2 implies G1 ./. N is commutative )
assume N = G2 ; :: thesis: G1 ./. N is commutative
then G1,G1 ./. N are_isomorphic by A2, A4, A6, A7, GROUP_6:82, TARSKI:def 2;
hence G1 ./. N is commutative by GROUP_6:89; :: thesis: verum

end;

hence ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) by A2, A4, A6, A7, 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 A2, Def1; :: thesis: verum