---

Step * 1 of Lemma left-opposite-between


1. e : OrientedPlane
2. b : Point
3. p : Point
4. q : Point
5. x : Point
6. q leftof pb
7. z : Point
8. Colinear(p;b;z)
9. z_q_x
⊢ x leftof pb
BY
{ (FLemma `left-convex3` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  OrientedPlane
2.  b  :  Point
3.  p  :  Point
4.  q  :  Point
5.  x  :  Point
6.  q  leftof  pb
7.  z  :  Point
8.  Colinear(p;b;z)
9.  z\_q\_x
\mvdash{}  x  leftof  pb


By

---

Latex:
(FLemma  `left-convex3`  [-1;-2]  THEN  Auto)

---

Home Index