---

Step * 1 of Lemma interval-connected


1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])
BY
{ (InstLemma `closed-interval-connected` [⌜rmin(a;b)⌝;⌜rmax(a;b)⌝]⋅ THENA Auto) }

1
1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
11. Connected({x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} )
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  I  :  Interval
2.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
6.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
7.  A[a]
8.  b  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  B[b]
10.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mvee{}  B[r])
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
(InstLemma  `closed-interval-connected`  [\mkleeneopen{}rmin(a;b)\mkleeneclose{};\mkleeneopen{}rmax(a;b)\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index