---

Step * 1 of Lemma i-finite-iff-bounded


1. I : Interval
2. i-finite(I)
⊢ ∃a,b:ℝ. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
BY
{ (InstConcl [⌜left-endpoint(I)⌝;⌜right-endpoint(I)⌝]⋅ THEN Auto) }

1
1. I : Interval
2. i-finite(I)
3. r : ℝ
4. r ∈ I
⊢ left-endpoint(I)≤r≤right-endpoint(I)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  i-finite(I)
\mvdash{}  \mexists{}a,b:\mBbbR{}.  \mforall{}[r:\mBbbR{}].  a\mleq{}r\mleq{}b  supposing  r  \mmember{}  I


By

---

Latex:
(InstConcl  [\mkleeneopen{}left-endpoint(I)\mkleeneclose{};\mkleeneopen{}right-endpoint(I)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index