---

Step * 1 1 2 1 1 3 of Lemma left-convex3


1. e : OrientedPlane
2. p : Point
3. b : Point
4. q : Point
5. x : Point
6. z : Point
7. q leftof bp
8. Colinear(b;p;z)
9. z_q_x
10. b ≠ p
11. p ≠ z
12. q # bp
13. q # zp
14. x # zp
⊢ x leftof bp
BY
{ (Assert x # bp BY
         ((Using [`a',⌜z⌝] (BLemma `colinear-lsep\'`)⋅ THENW Auto)
          THEN (Try (Trivial) THEN Try ((BLemma `geo-sep-sym` THEN Auto)))
          THEN RepeatFor 2 (ParallelOp 8)
          THEN Auto)) }

1
1. e : OrientedPlane
2. p : Point
3. b : Point
4. q : Point
5. x : Point
6. z : Point
7. q leftof bp
8. Colinear(b;p;z)
9. z_q_x
10. b ≠ p
11. p ≠ z
12. q # bp
13. q # zp
14. x # zp
15. x # bp
⊢ x leftof bp

---

Latex:

---

Latex:

1.  e  :  OrientedPlane
2.  p  :  Point
3.  b  :  Point
4.  q  :  Point
5.  x  :  Point
6.  z  :  Point
7.  q  leftof  bp
8.  Colinear(b;p;z)
9.  z\_q\_x
10.  b  \mneq{}  p
11.  p  \mneq{}  z
12.  q  \#  bp
13.  q  \#  zp
14.  x  \#  zp
\mvdash{}  x  leftof  bp


By

---

Latex:
(Assert  x  \#  bp  BY
              ((Using  [`a',\mkleeneopen{}z\mkleeneclose{}]  (BLemma  `colinear-lsep\mbackslash{}'`)\mcdot{}  THENW  Auto)
                THEN  (Try  (Trivial)  THEN  Try  ((BLemma  `geo-sep-sym`  THEN  Auto)))
                THEN  RepeatFor  2  (ParallelOp  8)
                THEN  Auto))

---

Home Index