---

Step * of Lemma left-convex2

∀g:EuclideanPlane. ∀a,b,x,y:Point.  (x leftof ab ⇒ (a_x_y ∨ (a_y_x ∧ y ≠ a)) ⇒ y leftof ab)
BY
{ Auto }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. a_x_y ∨ (a_y_x ∧ y ≠ a)
⊢ y leftof ab

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,x,y:Point.    (x  leftof  ab  {}\mRightarrow{}  (a\_x\_y  \mvee{}  (a\_y\_x  \mwedge{}  y  \mneq{}  a))  {}\mRightarrow{}  y  leftof  ab)


By

---

Latex:
Auto

---

Home Index