---

Step * of Lemma endpoints_wf

∀[I:Interval]. endpoints(I) ∈ ℝ × ℝ supposing i-finite(I)
BY
{ (Auto
   THEN D 1
   THEN (D 1 THEN RepUR ``i-finite`` (-1) THEN Auto)
   THEN D 2
   THEN Reduce (-1)
   THEN RepUR ``endpoints`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  endpoints(I)  \mmember{}  \mBbbR{}  \mtimes{}  \mBbbR{}  supposing  i-finite(I)


By

---

Latex:
(Auto
  THEN  D  1
  THEN  (D  1  THEN  RepUR  ``i-finite``  (-1)  THEN  Auto)
  THEN  D  2
  THEN  Reduce  (-1)
  THEN  RepUR  ``endpoints``  0
  THEN  Auto)

---

Home Index