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

proof

rng <*H*> c= the_normal_subgroups_of H

proof

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

end;

then reconsider F = <*H*> as FinSequence of the_normal_subgroups_of H by FINSEQ_1:def 4;
take F ; :: according to GRNILP_1:def 2 :: 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 normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) )
A2: len F = 1 by FINSEQ_1:39;
then A3: F . (len F) = H
.= (1). H by GROUP_2:63 ;
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )

proof

let i be Element of NAT ; :: thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; :: thesis: for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )
let G1, G2 be strict normal Subgroup of H; :: thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) )
assume ( G1 = F . i & G2 = F . (i + 1) ) ; :: thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )
dom F = {1} by A2, FINSEQ_1:2, FINSEQ_1:def 3;
then ( i = 1 & i + 1 = 1 ) by A4, TARSKI:def 1;
hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ; :: 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 normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) by A3, FINSEQ_1:40; :: thesis: verum

end;

thus H is strict ; :: thesis: verum