---

Step * of Lemma assert-inhabited-rat-interval

∀[I:ℚInterval]. uiff(↑Inhabited(I);(fst(I)) ≤ (snd(I)))
BY
{ ((D 0 THENA Auto) THEN D 1 THEN RepUR ``inhabited-rat-interval`` 0 THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:\mBbbQ{}Interval].  uiff(\muparrow{}Inhabited(I);(fst(I))  \mleq{}  (snd(I)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  1
  THEN  RepUR  ``inhabited-rat-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index