On Multiset Ordering

Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M₁ such that M₁(x) > N₁(x) and (∀y ∈ N₁)x ⊀ y. It should be M₁(x) ⩾ N₁(x). Nevertheless we do not know whether x ∈ N₁ or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].