---

Step * of Lemma dense-in-interval_wf

∀[I:Interval]. ∀[X:{a:ℝ| a ∈ I}  ⟶ ℙ].  (dense-in-interval(I;X) ∈ ℙ)
BY
{ ProveWfLemma }

1
1. I : Interval
2. X : {a:ℝ| a ∈ I}  ⟶ ℙ
3. ∀a:ℝ. (a ∈ I ∈ Type)
4. a : ℝ
5. a ∈ I
6. ∀r:ℝ. (r ∈ I ∈ Type)
7. b : ℝ
8. b ∈ I
9. a < b
10. x : ℝ
11. a < x
12. x < b
⊢ x ∈ {a:ℝ| a ∈ I} 

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[X:\{a:\mBbbR{}|  a  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}].    (dense-in-interval(I;X)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index