---

Step * 1 of Lemma sq_stable__icompact


1. x : ℝ@i
2. x2 : ℝ@i
3. ↓(∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))) ∧ (True ∧ True) ∧ True ∧ True@i
⊢ ∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))
BY
{ (Assert x ≤ x2 BY
         (D -1 THEN Unhide THEN Auto THEN ExRepD THEN Auto)) }

1
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))

---

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
\mvdash{}  \mexists{}r:\mBbbR{}.  ((x  \mleq{}  r)  \mwedge{}  (r  \mleq{}  x2))


By

---

Latex:
(Assert  x  \mleq{}  x2  BY
              (D  -1  THEN  Unhide  THEN  Auto  THEN  ExRepD  THEN  Auto))

---

Home Index