consider G being Group;
take H = (1). G; :: thesis: ( H is solvable & H is strict )
thus H is solvable :: thesis: H is strict

proof

<*H*> is FinSequence of Subgroups H

proof

rng <*H*> c= Subgroups H

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*H*> or x in Subgroups H )
assume A1: x in rng <*H*> ; :: thesis: x in Subgroups H
rng <*H*> = {H} by FINSEQ_1:56;
then x = H by A1, TARSKI:def 1;
then x is strict Subgroup of H by GROUP_2:63;
hence x in Subgroups H by GROUP_3:def 1; :: thesis: verum

end;

hence <*H*> is FinSequence of Subgroups H by FINSEQ_1:def 4; :: thesis: verum

end;

then reconsider F = <*H*> as FinSequence of Subgroups H ;
take F ; :: according to GRSOLV_1:def 1 :: thesis: ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of H 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 ) ) ) )
A2: len F = 1 by FINSEQ_1:56;
then A3: F . (len F) = H by FINSEQ_1:57
.= (1). H by GROUP_2:75 ;
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is 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 Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; :: thesis: for G1, G2 being Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
let G1, G2 be Subgroup of H; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
dom F = {1} by A2, FINSEQ_1:4, FINSEQ_1:def 3;
then ( i = 1 & i + 1 = 1 ) by A4, TARSKI:def 1;
hence ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ; :: thesis: verum

end;

hence ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of H 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 A2, A3, FINSEQ_1:57; :: thesis: verum

end;

thus H is strict ; :: thesis: verum