---

Step * of Lemma left-convex3

∀e:OrientedPlane. ∀b,p,q,x,z:Point.  (q leftof pb ⇒ Colinear(p;b;z) ⇒ z_q_x ⇒ x leftof pb)
BY
{ Auto }

1
1. e : OrientedPlane
2. b : Point
3. p : Point
4. q : Point
5. x : Point
6. z : Point
7. q leftof pb
8. Colinear(p;b;z)
9. z_q_x
⊢ x leftof pb

---

Latex:

---

Latex:
\mforall{}e:OrientedPlane.  \mforall{}b,p,q,x,z:Point.    (q  leftof  pb  {}\mRightarrow{}  Colinear(p;b;z)  {}\mRightarrow{}  z\_q\_x  {}\mRightarrow{}  x  leftof  pb)


By

---

Latex:
Auto

---

Home Index