---

Step * 2 of Lemma i-member-finite-closed


1. I : Interval@i
2. i-closed(I)@i
3. i-finite(I)@i
4. r : ℝ@i
5. left-endpoint(I)≤r≤right-endpoint(I)@i
⊢ r ∈ I
BY
{ (D (-1)
   THEN Auto
   THEN RepeatFor 2 (D 1)
   THEN D 2
   THEN ∀h:hyp. (RepUR ``i-finite`` h THEN Auto) 
   THEN D 1
   THEN D 2
   THEN ∀h:hyp. (RepUR ``i-closed`` h THEN SplitOrHyps THEN Auto) 
   THEN All (RepUR ``left-endpoint right-endpoint endpoints i-member``)
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  i-closed(I)@i
3.  i-finite(I)@i
4.  r  :  \mBbbR{}@i
5.  left-endpoint(I)\mleq{}r\mleq{}right-endpoint(I)@i
\mvdash{}  r  \mmember{}  I


By

---

Latex:
(D  (-1)
  THEN  Auto
  THEN  RepeatFor  2  (D  1)
  THEN  D  2
  THEN  \mforall{}h:hyp.  (RepUR  ``i-finite``  h  THEN  Auto) 
  THEN  D  1
  THEN  D  2
  THEN  \mforall{}h:hyp.  (RepUR  ``i-closed``  h  THEN  SplitOrHyps  THEN  Auto) 
  THEN  All  (RepUR  ``left-endpoint  right-endpoint  endpoints  i-member``)
  THEN  Auto)

---

Home Index