begin
theorem
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
canceled;
theorem Th11:
Lm1:
for G being Group
for A being Subgroup of G holds gr (carr A) is Subgroup of A
theorem Th12:
theorem
Lm2:
for G being Group
for A being Subgroup of G holds A is Subgroup of (Omega). G
theorem
theorem
Lm3:
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
theorem Th16:
:: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def 1 :
for G being Group
for b2 being set holds
( b2 = the_normal_subgroups_of G iff for x being set holds
( x in b2 iff x is strict normal Subgroup of G ) );
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem Def2 defines nilpotent GRNILP_1:def 2 :
for IT being Group holds
( IT is nilpotent iff ex F being FinSequence of the_normal_subgroups_of IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( 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 IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ) );
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm4:
for G being Group
for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
Lm5:
for G being Group
for F1 being strict Subgroup of G
for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem