begin
theorem Th1:
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
:: deftheorem Def1 defines |^ GROUP_5:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
begin
:: deftheorem defines [. GROUP_5:def 2 :
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th39:
Lm1:
for G being commutative Group
for a, b being Element of G holds a * b = b * a
;
theorem
theorem Th41:
:: deftheorem defines [. GROUP_5:def 3 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines commutators GROUP_5:def 4 :
theorem
canceled;
theorem Th52:
theorem
theorem
theorem Th55:
theorem Th56:
:: deftheorem defines commutators GROUP_5:def 5 :
theorem
canceled;
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
:: deftheorem defines commutators GROUP_5:def 6 :
theorem
canceled;
theorem Th65:
theorem
:: deftheorem defines [. GROUP_5:def 7 :
theorem
canceled;
theorem Th68:
theorem Th69:
theorem
:: deftheorem defines [. GROUP_5:def 8 :
theorem
canceled;
theorem
theorem
theorem Th74:
theorem
theorem
theorem Th77:
Lm2:
for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
theorem Th78:
theorem Th79:
theorem
:: deftheorem defines ` GROUP_5:def 9 :
theorem
canceled;
theorem
theorem Th83:
theorem Th84:
theorem
theorem
begin
:: deftheorem Def10 defines center GROUP_5:def 10 :
theorem
canceled;
theorem
canceled;
theorem Th89:
theorem
theorem
theorem
theorem
theorem