---

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

.....assertion..... 
1. ∃c:ℝ
    (((r0 ≤ c) ∧ (c < r1))
    ∧ (∀[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)))))))))
2. [A] : ℝ ⟶ ℙ
3. [B] : ℝ ⟶ ℙ
4. ∃a:ℝ. A[a]
5. ∃b:ℝ. B[b]
6. ∀r:ℝ. (A[r] ∨ B[r])
⊢ ∃a,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))
BY
{ (Thin 1 THEN ExRepD THEN (InstLemma `rless-cases` [⌜r0⌝;⌜r1⌝;⌜a⌝]⋅ THENA Auto) THEN D -1) }

1
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. ∀r:ℝ. (A[r] ∨ B[r])
8. r0 < a
⊢ ∃a,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))

2
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. ∀r:ℝ. (A[r] ∨ B[r])
8. a < r1
⊢ ∃a,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))

---

Latex:

---

Latex:
.....assertion..... 
1.  \mexists{}c:\mBbbR{}
        (((r0  \mleq{}  c)  \mwedge{}  (c  <  r1))
        \mwedge{}  (\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)))))))))
2.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}a:\mBbbR{}.  A[a]
5.  \mexists{}b:\mBbbR{}.  B[b]
6.  \mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r])
\mvdash{}  \mexists{}a,b:\mBbbR{}.  ((A  a)  \mwedge{}  (B  b)  \mwedge{}  ((a  \mleq{}  b)  \mvee{}  (b  \mleq{}  a)))


By

---

Latex:
(Thin  1  THEN  ExRepD  THEN  (InstLemma  `rless-cases`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index