---

Step * of Lemma rv-inner-Pasch''

∀n:ℕ. ∀a,b,c,p,q:ℝ^n.
  (a-p-c
  ⇒ b-q-c
  ⇒ (∃x:ℝ^n. ((¬(a ≠ x ∧ x ≠ q ∧ (¬a-x-q))) ∧ (¬(b ≠ x ∧ x ≠ p ∧ (¬b-x-p))) ∧ (a ≠ q ⇒ a-x-q) ∧ (b ≠ p ⇒ b-x-p))))
BY
{ (InstLemma `rv-inner-Pasch\'` [] THEN RepeatFor 9 ((ParallelLast' THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c,p,q:\mBbbR{}\^{}n.
    (a-p-c
    {}\mRightarrow{}  b-q-c
    {}\mRightarrow{}  (\mexists{}x:\mBbbR{}\^{}n
              ((\mneg{}(a  \mneq{}  x  \mwedge{}  x  \mneq{}  q  \mwedge{}  (\mneg{}a-x-q)))
              \mwedge{}  (\mneg{}(b  \mneq{}  x  \mwedge{}  x  \mneq{}  p  \mwedge{}  (\mneg{}b-x-p)))
              \mwedge{}  (a  \mneq{}  q  {}\mRightarrow{}  a-x-q)
              \mwedge{}  (b  \mneq{}  p  {}\mRightarrow{}  b-x-p))))


By

---

Latex:
(InstLemma  `rv-inner-Pasch\mbackslash{}'`  []  THEN  RepeatFor  9  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index