@misc{BAGORD_2.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {On Multiset Ordering}, 
  ADDRESS1 = {Association of Mizar Users, Bia{\l}ystok},
  SECTION1 = {Preliminaries},
  SECTION2 = {},
  SECTION3 = {},
  SECTION4 = {},
  YEAR = {2015},
  MONTH = {December},
  DAY = {31},
  SUMMARY = {Formalization of a part of \cite{JouannaudLescanne}.
  Unfortunately, not all is able to be formalized.
  Namely, in the paper is mistake in the proof of Lemma 3.
  There is stated that there exists $x\in M_1$ such that $M_1(x)>N_1(x)$ and
  $(\forall y\in N_1)x\not\prec y$. There should be $M_1(x)\geq N_1(x)$.
  Nevertheless we do not know whether $x\in N_1$ or not and cannot prove the
  contradiction.}}

@Article{JouannaudLescanne,
  author = 	 {Jean-Pierre Jouannaud and Pierre Lescanne},
  title = 	 {On Multiset Ordering},
  journal = 	 {Information Processing Letters},
  year = 	 {1982},
  volume =	 {15},
  number =	 {2},
  pages =	 {57--63},
  doi = 	 {10.1016/0020-0190(82)90107-7}}

