@MISC{BAGORDER.MIZ,
  AUTHOR = {Lee, Gilbert and Rudnicki, Piotr},
  TITLE = {On Ordering of Bags},
  SECTION1 = {Preliminaries},
  SECTION2 = {More About Bags},
  SECTION3 = {Some Special Orders},
  SECTION4 = {Ordering of Finite Subsets},
  DAY = {12},
  MONTH = {March},
  YEAR = {2002},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {University of Alberta\\Edmonton},
  SUMMARY = {We present a Mizar formalization of chapter 4.4 of \cite{Becker93}
  devoted to special orderings in additive monoids to be used for ordering
  terms in multivariate polynomials.  We have extended the
  treatment to the case of infinite number of variables.  It turns out that
  in such case admissible orderings are not necessarily well orderings.}}

