---

Step * 1 of Lemma i-approx-elim

.....set predicate..... 
1. I : Interval
2. n : ℕ+
3. i-nonvoid(i-approx(I;n))
4. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
⊢ left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))
BY
{ ((HypSubst' (-1) (-2) THEN Thin (-1)) THEN RepUR ``i-nonvoid`` -1 THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  I  :  Interval
2.  n  :  \mBbbN{}\msupplus{}
3.  i-nonvoid(i-approx(I;n))
4.  i-approx(I;n)  \msim{}  [left-endpoint(i-approx(I;n)),  right-endpoint(i-approx(I;n))]
\mvdash{}  left-endpoint(i-approx(I;n))  \mleq{}  right-endpoint(i-approx(I;n))


By

---

Latex:
((HypSubst'  (-1)  (-2)  THEN  Thin  (-1))  THEN  RepUR  ``i-nonvoid``  -1  THEN  ExRepD  THEN  Auto)

---

Home Index