---

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

.....assertion..... 
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
15. x # bp
16. x leftof bp
⊢ False
BY
{ ((InstLemma `lsep-opposite-iff` [⌜e⌝;⌜b⌝;⌜p⌝;⌜q⌝;⌜x⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin  (-2)
   THEN (D -1 THENA (Auto THEN FLemma `not-left-and-right` [-1] THEN Auto))
   THEN D -1
   THEN RenameVar `w' (-2)
   THEN D -1) }

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
14. x # zp
15. x # bp
16. x leftof bp
17. w : Point
18. q_w_x
19. Colinear(w;b;p)
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
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
14.  x  \#  zp
15.  x  \#  bp
16.  x  leftof  bp
\mvdash{}  False


By

---

Latex:
((InstLemma  `lsep-opposite-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin    (-2)
  THEN  (D  -1  THENA  (Auto  THEN  FLemma  `not-left-and-right`  [-1]  THEN  Auto))
  THEN  D  -1
  THEN  RenameVar  `w'  (-2)
  THEN  D  -1)

---

Home Index