---

Step * 2 of Lemma mu-ge_wf2


1. n : ℤ
2. f : {n...} ⟶ (Top + Top)
3. m : {n...}
4. ↑isl(f m)
5. ∀d:ℕ. ((n ≤ (m - d)) ⇒ (mu-ge(f;m - d) ∈ {n...}))
⊢ mu-ge(f;n) ∈ {n...}
BY
{ ((InstHyp [⌜m - n⌝] (-1)⋅ THENA Auto) THEN NthHypSq (-1) THEN RepeatFor 2 (EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  f  :  \{n...\}  {}\mrightarrow{}  (Top  +  Top)
3.  m  :  \{n...\}
4.  \muparrow{}isl(f  m)
5.  \mforall{}d:\mBbbN{}.  ((n  \mleq{}  (m  -  d))  {}\mRightarrow{}  (mu-ge(f;m  -  d)  \mmember{}  \{n...\}))
\mvdash{}  mu-ge(f;n)  \mmember{}  \{n...\}


By

---

Latex:
((InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  NthHypSq  (-1)  THEN  RepeatFor  2  (EqCD)  THEN  Auto)

---

Home Index