---

Step * 2 of Lemma lsep-opposite-iff


1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ba
7. y leftof ba
8. z : Point
9. x_z_y
10. Colinear(z;a;b)
11. y leftof ba
⊢ x leftof ab
BY
{ (Thin (-1)
   THEN FLemma `left-between` [6;7;-2]⋅
   THEN Auto
   THEN (RWO  "not-lsep-iff-colinear<" (-2) THENA Auto)
   THEN D -2
   THEN Unfold `geo-lsep` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  a  :  Point
3.  b  :  Point
4.  x  :  Point
5.  y  :  Point
6.  x  leftof  ba
7.  y  leftof  ba
8.  z  :  Point
9.  x\_z\_y
10.  Colinear(z;a;b)
11.  y  leftof  ba
\mvdash{}  x  leftof  ab


By

---

Latex:
(Thin  (-1)
  THEN  FLemma  `left-between`  [6;7;-2]\mcdot{}
  THEN  Auto
  THEN  (RWO    "not-lsep-iff-colinear<"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  Unfold  `geo-lsep`  0
  THEN  Auto)

---

Home Index