---

Step * of Lemma full-Pasch-lemma

No Annotations
∀e:EuclideanPlane. ∀a,x,y,d,p:Point.
  ((((d leftof xa ∧ x-p-a) ∧ d # py) ∧ a leftof xy) ⇒ (∃p':Point. ((x-p'-y ∨ a-p'-y) ∧ Colinear(d;p;p'))))
BY
{ (Auto THEN (Assert y leftof ax BY RepeatFor 2 ((FLemma `left-symmetry` [-1] THEN Auto)))) }

1
1. e : EuclideanPlane
2. a : Point
3. x : Point
4. y : Point
5. d : Point
6. p : Point
7. d leftof xa
8. x-p-a
9. d # py
10. a leftof xy
11. y leftof ax
⊢ ∃p':Point. ((x-p'-y ∨ a-p'-y) ∧ Colinear(d;p;p'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,x,y,d,p:Point.
    ((((d  leftof  xa  \mwedge{}  x-p-a)  \mwedge{}  d  \#  py)  \mwedge{}  a  leftof  xy)
    {}\mRightarrow{}  (\mexists{}p':Point.  ((x-p'-y  \mvee{}  a-p'-y)  \mwedge{}  Colinear(d;p;p'))))


By

---

Latex:
(Auto  THEN  (Assert  y  leftof  ax  BY  RepeatFor  2  ((FLemma  `left-symmetry`  [-1]  THEN  Auto))))

---

Home Index