let G be Group; :: thesis: ( ex F being FinSequence of Subgroups 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, 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 cyclic Group ) ) ) ) implies G is solvable )
given F being FinSequence of Subgroups G such that A1: ( 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, 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 cyclic Group ) ) ) ) ; :: thesis: G is solvable
take F ; :: according to GRSOLV_1:def 1 :: thesis: ( 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, 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 ) ) ) )
thus ( 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, 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 ) ) ) ) by A1; :: thesis: verum