begin
theorem
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
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 Th19:
:: deftheorem def2 defines the_normal_subgroups_of GRNILP_1:def 1 :
theorem Th40:
theorem Th21:
theorem Th39:
:: deftheorem def3 defines nilpotent GRNILP_1:def 2 :
theorem Th22:
theorem Th24:
theorem Th25:
theorem Th26:
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 Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem
theorem