---

Step * 1 1 1 of Lemma closed-interval-connected


1. u : ℝ
2. v : ℝ
3. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
4. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
7. a : {x:ℝ| x ∈ [u, v]} 
8. A[a]
9. b : {x:ℝ| x ∈ [u, v]} 
10. B[b]
11. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
12. u ≤ v
13. (∃a:ℝ. (A interval-retraction(u;v;a)))
⇒ (∃b:ℝ. (B interval-retraction(u;v;b)))
⇒ (∀r:ℝ. ((A interval-retraction(u;v;r)) ∨ (B interval-retraction(u;v;r))))
⇒ (∃r:ℝ. ((A interval-retraction(u;v;r)) ∧ (B interval-retraction(u;v;r))))
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])
BY
{ ((D -1 THENA (D 0 With ⌜a⌝  THEN Auto)) THEN (D -1 THENA (D 0 With ⌜b⌝  THEN Auto))) }

1
1. u : ℝ
2. v : ℝ
3. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
4. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
7. a : {x:ℝ| x ∈ [u, v]} 
8. A[a]
9. b : {x:ℝ| x ∈ [u, v]} 
10. B[b]
11. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
12. u ≤ v
13. (∀r:ℝ. ((A interval-retraction(u;v;r)) ∨ (B interval-retraction(u;v;r))))
⇒ (∃r:ℝ. ((A interval-retraction(u;v;r)) ∧ (B interval-retraction(u;v;r))))
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
4.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
6.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
7.  a  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
8.  A[a]
9.  b  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
10.  B[b]
11.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mvee{}  B[r])
12.  u  \mleq{}  v
13.  (\mexists{}a:\mBbbR{}.  (A  interval-retraction(u;v;a)))
{}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  (B  interval-retraction(u;v;b)))
{}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  ((A  interval-retraction(u;v;r))  \mvee{}  (B  interval-retraction(u;v;r))))
{}\mRightarrow{}  (\mexists{}r:\mBbbR{}.  ((A  interval-retraction(u;v;r))  \mwedge{}  (B  interval-retraction(u;v;r))))
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((D  -1  THENA  (D  0  With  \mkleeneopen{}a\mkleeneclose{}    THEN  Auto))  THEN  (D  -1  THENA  (D  0  With  \mkleeneopen{}b\mkleeneclose{}    THEN  Auto)))

---

Home Index