---

Step * 1 1 1 1 of Lemma left-convex3


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
10. p ≠ b
11. p ≠ z
12. q # bp
13. q # zp
⊢ x leftof pb
BY
{ (Assert x # zp BY
         ((Using [`a',⌜q⌝] (BLemma `colinear-lsep`)⋅ THENW Auto) THEN Try (Trivial))) }

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
10. p ≠ b
11. p ≠ z
12. q # bp
13. q # zp
⊢ x ≠ z

2
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
10. p ≠ b
11. p ≠ z
12. q # bp
13. q # zp
⊢ Colinear(x;q;z)

3
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
10. p ≠ b
11. p ≠ z
12. q # bp
13. q # zp
14. x # zp
⊢ x leftof pb

---

Latex:

---

Latex:

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
10.  p  \mneq{}  b
11.  p  \mneq{}  z
12.  q  \#  bp
13.  q  \#  zp
\mvdash{}  x  leftof  pb


By

---

Latex:
(Assert  x  \#  zp  BY
              ((Using  [`a',\mkleeneopen{}q\mkleeneclose{}]  (BLemma  `colinear-lsep`)\mcdot{}  THENW  Auto)  THEN  Try  (Trivial)))

---

Home Index