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

proof

rng <*H*> c= Subgroups H

proof

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

end;

then reconsider F = <*H*> as FinSequence of Subgroups H by FINSEQ_1:def 4;
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:39;
A3: 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 that
A4: i in dom F and
A5: 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 that
G1 = F . i and
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 ) )
A6: dom F = {1} by A2, FINSEQ_1:2, FINSEQ_1:def 3;
then i = 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 ) ) by A5, A6, TARSKI:def 1; :: thesis: verum

end;

F . (len F) = H by A2
.= (1). H by GROUP_2:63 ;
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; :: thesis: verum

end;

thus H is strict ; :: thesis: verum