---

Step * of Lemma closed-interval-connected

∀u,v:ℝ.  Connected({x:ℝ| x ∈ [u, v]} )
BY
{ (Auto
   THEN InstLemma `reals-connected` []
   THEN ParallelLast
   THEN Auto
   THEN ExRepD
   THEN (Assert u ≤ v BY
               ((Assert a ∈ [u, v] BY Auto) THEN Reduce -1 THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}u,v:\mBbbR{}.    Connected(\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  )


By

---

Latex:
(Auto
  THEN  InstLemma  `reals-connected`  []
  THEN  ParallelLast
  THEN  Auto
  THEN  ExRepD
  THEN  (Assert  u  \mleq{}  v  BY
                          ((Assert  a  \mmember{}  [u,  v]  BY  Auto)  THEN  Reduce  -1  THEN  Auto)))

---

Home Index