---

Step * of Lemma eu-inner-pasch-ex

∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| ¬Colinear(a;b;c)} . ∀p:{p:Point| a-p-c} . ∀q:{q:Point| b_q_c} .
  ∃x:Point. (p-x-b ∧ q-x-a ∧ (x = eu-inner-pasch(e;a;b;c;p;q) ∈ Point))
BY
{ Auto }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : {c:Point| ¬Colinear(a;b;c)} @i
5. p : {p:Point| a-p-c} @i
6. q : {q:Point| b_q_c} @i
⊢ ∃x:Point. (p-x-b ∧ q-x-a ∧ (x = eu-inner-pasch(e;a;b;c;p;q) ∈ Point))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  .  \mforall{}p:\{p:Point|  a-p-c\}  .  \mforall{}q:\{q:Point| 
                                                                                                                                                                                b\_q\_c\}  .
    \mexists{}x:Point.  (p-x-b  \mwedge{}  q-x-a  \mwedge{}  (x  =  eu-inner-pasch(e;a;b;c;p;q)))


By

---

Latex:
Auto

---

Home Index