---

Step * of Lemma interval-connected

∀I:Interval. Connected({x:ℝ| x ∈ I} )
BY
{ (Auto THEN D 0 THEN Auto THEN ExRepD) }

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])
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])

---

Latex:

---

Latex:
\mforall{}I:Interval.  Connected(\{x:\mBbbR{}|  x  \mmember{}  I\}  )


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  ExRepD)

---

Home Index