---

Step * of Lemma is-half-interval-sub-interval

No Annotations
∀I,J:ℚInterval.  (rat-sub-interval(I;J)) supposing ((↑is-half-interval(I;J)) and (↑Inhabited(J)))
BY
{ ((Auto THEN D 2 THEN D 1)
   THEN All (RepUR ``is-half-interval rat-sub-interval inhabited-rat-interval``)
   THEN (All (RW assert_pushdownC) THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN QavgSimp 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,J:\mBbbQ{}Interval.    (rat-sub-interval(I;J))  supposing  ((\muparrow{}is-half-interval(I;J))  and  (\muparrow{}Inhabited(J)))


By

---

Latex:
((Auto  THEN  D  2  THEN  D  1)
  THEN  All  (RepUR  ``is-half-interval  rat-sub-interval  inhabited-rat-interval``)
  THEN  (All  (RW  assert\_pushdownC)  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  QavgSimp  0
  THEN  Auto)

---

Home Index