---

Step * of Lemma half-point-interval

∀[I:ℚInterval]. ∀[a:ℚ].  I = [a] ∈ ℚInterval supposing ↑is-half-interval(I;[a])
BY
{ ((Auto THEN D 1 THEN RepUR ``is-half-interval`` -1 THEN (RW assert_pushdownC (-1) THENA Auto))
   THEN QavgSimp (-1)
   THEN Unfold `rat-point-interval` 0
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:\mBbbQ{}Interval].  \mforall{}[a:\mBbbQ{}].    I  =  [a]  supposing  \muparrow{}is-half-interval(I;[a])


By

---

Latex:
((Auto  THEN  D  1  THEN  RepUR  ``is-half-interval``  -1  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))
  THEN  QavgSimp  (-1)
  THEN  Unfold  `rat-point-interval`  0
  THEN  D  -1
  THEN  Auto)

---

Home Index