---

Step * of Lemma i-type-member

∀I:Interval. ∀p:i-type(I).  (real(p) ∈ I)
BY
{ (Auto
   THEN D -1
   THEN RepUR ``i-real`` 0
   THEN (BLemma `i-member-iff` THEN Auto)
   THEN InstConcl [⌜n⌝]⋅
   THEN Auto
   THEN D (-1)
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}p:i-type(I).    (real(p)  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  RepUR  ``i-real``  0
  THEN  (BLemma  `i-member-iff`  THEN  Auto)
  THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Unhide
  THEN  Auto)

---

Home Index