---

Step * of Lemma no-real-separation-corollary

∀[A,B:ℝ ⟶ ℙ].  ((∃x:ℝ. A[x]) ⇒ (∃y:ℝ. B[y]) ⇒ (∀r:ℝ. (A[r] ∨ B[r])) ⇒ (¬¬(∃x,y:ℝ. ((x = y) ∧ A[x] ∧ B[y]))))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (InstLemma `no-real-separation` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}x:\mBbbR{}.  A[x])  {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  B[y])  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}x,y:\mBbbR{}.  ((x  =  y)  \mwedge{}  A[x]  \mwedge{}  B[y]))))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `no-real-separation`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index