---

Step * 1 1 of Lemma sq_stable__icompact


1. x : ℝ@i
2. x2 : ℝ@i
3. ↓(∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))) ∧ (True ∧ True) ∧ True ∧ True@i
4. x ≤ x2
⊢ ∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))
BY
{ (With ⌜x⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  x2  :  \mBbbR{}@i
3.  \mdownarrow{}(\mexists{}r:\mBbbR{}.  ((x  \mleq{}  r)  \mwedge{}  (r  \mleq{}  x2)))  \mwedge{}  (True  \mwedge{}  True)  \mwedge{}  True  \mwedge{}  True@i
4.  x  \mleq{}  x2
\mvdash{}  \mexists{}r:\mBbbR{}.  ((x  \mleq{}  r)  \mwedge{}  (r  \mleq{}  x2))


By

---

Latex:
(With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index