---

Step * of Lemma rccint-icompact

∀a,b:ℝ.  (a ≤ b ⇐⇒ icompact([a, b]))
BY
{ (RepUR ``icompact rccint i-closed i-finite i-nonvoid i-member`` 0
   THEN Auto
   THEN ExRepD
   THEN Try ((RelRST THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    (a  \mleq{}  b  \mLeftarrow{}{}\mRightarrow{}  icompact([a,  b]))


By

---

Latex:
(RepUR  ``icompact  rccint  i-closed  i-finite  i-nonvoid  i-member``  0
  THEN  Auto
  THEN  ExRepD
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index