---

Step * of Lemma outer-Pasch

No Annotations
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| B(abc)} . ∀x:Point. ∀y:{y:Point| b-x-y} .
  (x # ab ⇒ (∃p:Point [(B(axp) ∧ B(cpy))]))
BY
{ (Auto THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : {c:Point| B(abc)} 
5. x : Point
6. y : {y:Point| b-x-y} 
7. x leftof ab
⊢ ∃p:Point [(B(axp) ∧ B(cpy))]

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : {c:Point| B(abc)} 
5. x : Point
6. y : {y:Point| b-x-y} 
7. x leftof ba
⊢ ∃p:Point [(B(axp) ∧ B(cpy))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  B(abc)\}  .  \mforall{}x:Point.  \mforall{}y:\{y:Point|  b-x-y\}  .
    (x  \#  ab  {}\mRightarrow{}  (\mexists{}p:Point  [(B(axp)  \mwedge{}  B(cpy))]))


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index