---

Step * of Lemma i-member-compact

∀I:Interval. (icompact(I) ⇒ (∀r:ℝ. (r ∈ I ⇐⇒ left-endpoint(I)≤r≤right-endpoint(I))))
BY
{ ((InstLemma `i-member-finite-closed` [])
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN (D -1 THENA Auto)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (r  \mmember{}  I  \mLeftarrow{}{}\mRightarrow{}  left-endpoint(I)\mleq{}r\mleq{}right-endpoint(I))))


By

---

Latex:
((InstLemma  `i-member-finite-closed`  [])
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  (D  -1  THENA  Auto)
  THEN  Trivial)

---

Home Index