---

Step * of Lemma i-member-finite-closed

∀I:Interval. (i-closed(I) ⇒ i-finite(I) ⇒ (∀r:ℝ. (r ∈ I ⇐⇒ left-endpoint(I)≤r≤right-endpoint(I))))
BY
{ Auto }

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

2
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

---

Latex:

---

Latex:
\mforall{}I:Interval
    (i-closed(I)  {}\mRightarrow{}  i-finite(I)  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (r  \mmember{}  I  \mLeftarrow{}{}\mRightarrow{}  left-endpoint(I)\mleq{}r\mleq{}right-endpoint(I))))


By

---

Latex:
Auto

---

Home Index