@MISC{GROUP_8.MIZ,
  AUTHOR = {Geleijnse, Gijs and Bancerek, Grzegorz},
  TITLE = {Properties of Groups},
  NOTE = {This work has been partially supported by the CALCULEMUS
      grant HPRN-CT-2000-00102.},
  ACKNOWLEDGEMENT = {???? The Mizar Group is thanked for their help and hospitality.},
  DAY = {31},
  MONTH = {May},
  YEAR = {2004},
  ADDRESS1 = {Eindhoven University of Technology},
  ADDRESS2 = {Bia{\l}ystok Technical University},
  SUMMARY = {In this article we formalize theorems from Chapter 1
   of \cite{Hall:1959}. Our article covers
   Theorems 1.5.4, 1.5.5
   (inequality on indices),
   1.5.6 (equality of indices), Lemma 1.6.1 and several
   other supporting theorems needed to complete the formalization.}}

