---

Step * of Lemma compact-proper-interval-near-member

∀J:Interval
  (icompact(J)
  ⇒ iproper(J)
  ⇒ (∀x:ℝ. ((x ∈ J) ⇒ (∀r:ℝ. ((r0 < r) ⇒ (∃y:ℝ. ((y ∈ J) ∧ (|y - x| ≤ r) ∧ (r0 < |y - x|))))))))
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN DProdsAndUnions
   THEN RepUR ``icompact i-closed i-nonvoid i-finite iproper`` 0
   THEN RepUR ``left-endpoint right-endpoint endpoints i-member`` 0
   THEN Auto
   THEN RenameVar `a' 1
   THEN RenameVar `b' 2
   THEN RenameVar `x' (-5)
   THEN (Assert a < b BY
               Auto)
   THEN RepeatFor 6 (Thin (-7))) }

1
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. a ≤ x
5. x ≤ b
6. r : ℝ
7. r0 < r
8. a < b
⊢ ∃y:ℝ. (((a ≤ y) ∧ (y ≤ b)) ∧ (|y - x| ≤ r) ∧ (r0 < |y - x|))

---

Latex:

---

Latex:
\mforall{}J:Interval
    (icompact(J)
    {}\mRightarrow{}  iproper(J)
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  J)  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  ((r0  <  r)  {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  ((y  \mmember{}  J)  \mwedge{}  (|y  -  x|  \mleq{}  r)  \mwedge{}  (r0  <  |y  -  x|))))))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  DProdsAndUnions
  THEN  RepUR  ``icompact  i-closed  i-nonvoid  i-finite  iproper``  0
  THEN  RepUR  ``left-endpoint  right-endpoint  endpoints  i-member``  0
  THEN  Auto
  THEN  RenameVar  `a'  1
  THEN  RenameVar  `b'  2
  THEN  RenameVar  `x'  (-5)
  THEN  (Assert  a  <  b  BY
                          Auto)
  THEN  RepeatFor  6  (Thin  (-7)))

---

Home Index