---

Step * 1 1 2 1 of Lemma mfact_exists


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. WellFnd{i}(|g|;x,y.x p| y)
4. ∀c:|g|. Dec(Reducible(c))
5. j : |g|
6. ∀k:|g|. ((k p| j) ⇒ (¬(g-unit(k))) ⇒ (∃as:Atom{g} List. (k = (Π as) ∈ |g|)))
7. ¬(g-unit(j))
8. ¬Reducible(j)
⊢ j ∈ Atom{g}
BY
{ ((MemTypeCD) THEN Auto) }

1
.....set predicate..... 
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. WellFnd{i}(|g|;x,y.x p| y)
4. ∀c:|g|. Dec(Reducible(c))
5. j : |g|
6. ∀k:|g|. ((k p| j) ⇒ (¬(g-unit(k))) ⇒ (∃as:Atom{g} List. (k = (Π as) ∈ |g|)))
7. ¬(g-unit(j))
8. ¬Reducible(j)
⊢ Atomic(j)

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  WellFnd\{i\}(|g|;x,y.x  p|  y)
4.  \mforall{}c:|g|.  Dec(Reducible(c))
5.  j  :  |g|
6.  \mforall{}k:|g|.  ((k  p|  j)  {}\mRightarrow{}  (\mneg{}(g-unit(k)))  {}\mRightarrow{}  (\mexists{}as:Atom\{g\}  List.  (k  =  (\mPi{}  as))))
7.  \mneg{}(g-unit(j))
8.  \mneg{}Reducible(j)
\mvdash{}  j  \mmember{}  Atom\{g\}


By

---

Latex:
((MemTypeCD)  THEN  Auto)

---

Home Index