---

Step * 1 1 2 1 1 of Lemma i-approx-rep


1. x1 : ℝ
2. x2 : ℝ
3. ∃r:ℝ. (r ∈ <inl inl x1, inl inl x2>)
4. True
5. True
6. True
7. True
⊢ <inl inl x1, inl inl x2> = [left-endpoint(<inl inl x1, inl inl x2>), right-endpoint(<inl inl x1, inl inl x2>)] ∈ Inter\000Cval
BY
{ (Fold `rccint` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  x1  :  \mBbbR{}
2.  x2  :  \mBbbR{}
3.  \mexists{}r:\mBbbR{}.  (r  \mmember{}  <inl  inl  x1,  inl  inl  x2>)
4.  True
5.  True
6.  True
7.  True
\mvdash{}  <inl  inl  x1,  inl  inl  x2>  =  [left-endpoint(<inl  inl  x1,  inl  inl  x2>),  right-endpoint(<inl  inl  x1,  i\000Cnl  inl  x2>)]


By

---

Latex:
(Fold  `rccint`  0  THEN  EqCD  THEN  Auto)

---

Home Index