@MISC{GROUP_9.MIZ,
  AUTHOR = {Riccardi, Marco},
  TITLE = {The {J}ordan-{H}\"older Theorem},
  SECTION1 = {Actions and Groups with Operators},
  SECTION2 = {Some Theorems on Groups reformulated for Groups with Operators},
  SECTION3 = {Others Theorems on Actions and Groups with Operators},
  SECTION4 = {The Zassenhaus Butterfly Lemma},
  SECTION5 = {Composition Series},
  SECTION6 = {The Schreier Refinement Theorem},
  SECTION7 = {The Jordan-H\"older Theorem},
  SECTION8 = {Appendix},
  DAY = {20},
  MONTH = {April},
  YEAR = {2007},
  ADDRESS1 = {Casella Postale 49\\54038 Montignoso\\Italy},
  SUMMARY = {The goal of this article is to formalize
  the Jordan-H\"older theorem in the context of group with
  operators as in the book \cite{BourbakiAlgI}. In doing it,
  the article introduces the structure of group with operators and reformulates
  some theorems on group already present in Mizar Mathematical Library.
  Next, the article formalizes the Zassenhaus butterfly lemma
  and the Schreier refinement theorem, and defines the composition series.
  The appendix contains some theorems on mathematical objects that
  must belong to other articles.}}

@BOOK{BourbakiAlgI,
       AUTHOR = {Bourbaki, Nicolas},
        TITLE = {Elements of Mathematics. Algebra I. Chapters 1--3},
    PUBLISHER = {Springer-Verlag},
         YEAR = {1989},
      ADDRESS = {Berlin Heidelberg New York London Paris Tokyo}}

