---

Step * 2 2 3 1 of Lemma inhabited-covers-reals-implies


1. c : ℝ
2. r0 ≤ c
3. c < r1
4. ∀[A,B:ℝ ⟶ ℙ].
     ((∀r:ℝ. (A[r] ∨ B[r]))
     ⇒ (∀a,b:ℝ.
           (((A a) ∧ (B b) ∧ (a ≤ b))
           ⇒ (∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))))
5. [A] : ℝ ⟶ ℙ
6. [B] : ℝ ⟶ ℙ
7. ∃a:ℝ. A[a]
8. ∃b:ℝ. B[b]
9. ∀r:ℝ. (A[r] ∨ B[r])
10. a : ℝ
11. b : ℝ
12. A a
13. B b
14. b ≤ a
15. r : ℝ
⊢ B[r] ∨ A[r]
BY
{ ((Assert A[r] ∨ B[r] BY Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}
2.  r0  \mleq{}  c
3.  c  <  r1
4.  \mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
          ((\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
          {}\mRightarrow{}  (\mforall{}a,b:\mBbbR{}.
                      (((A  a)  \mwedge{}  (B  b)  \mwedge{}  (a  \mleq{}  b))
                      {}\mRightarrow{}  (\mexists{}a',b':\mBbbR{}
                                ((A  a')
                                \mwedge{}  (B  b')
                                \mwedge{}  (a  \mleq{}  a')
                                \mwedge{}  (a'  \mleq{}  b')
                                \mwedge{}  (b'  \mleq{}  b)
                                \mwedge{}  ((b'  -  a')  \mleq{}  ((b  -  a)  *  c)))))))
5.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
6.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
7.  \mexists{}a:\mBbbR{}.  A[a]
8.  \mexists{}b:\mBbbR{}.  B[b]
9.  \mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r])
10.  a  :  \mBbbR{}
11.  b  :  \mBbbR{}
12.  A  a
13.  B  b
14.  b  \mleq{}  a
15.  r  :  \mBbbR{}
\mvdash{}  B[r]  \mvee{}  A[r]


By

---

Latex:
((Assert  A[r]  \mvee{}  B[r]  BY  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index