---

Step * 1 2 of Lemma geo-left-interiority


1. g : OrientedPlane
2. x : Point
3. a : Point
4. b : Point
5. c : Point
6. p : Point
7. p leftof xb
8. p leftof bc
9. p leftof cx
10. x leftof cb
11. Colinear(c;b;x)
12. B(xxp)
13. a ≡ x
⊢ False
BY
{ ((Assert x # cb BY
          (OrLeft THEN Auto))
   THEN MoveToConcl  (-1)
   THEN Fold `not` 0
   THEN RWO "not-lsep-iff-colinear" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  x  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  p  :  Point
7.  p  leftof  xb
8.  p  leftof  bc
9.  p  leftof  cx
10.  x  leftof  cb
11.  Colinear(c;b;x)
12.  B(xxp)
13.  a  \mequiv{}  x
\mvdash{}  False


By

---

Latex:
((Assert  x  \#  cb  BY
                (OrLeft  THEN  Auto))
  THEN  MoveToConcl    (-1)
  THEN  Fold  `not`  0
  THEN  RWO  "not-lsep-iff-colinear"  0
  THEN  Auto)

---

Home Index