---

Step * 4 1 of Lemma lsep-opposite-iff


1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ba
8. x leftof ab ⇐ y leftof ba
9. y leftof ba
10. x1 : Point
11. Colinear(a;b;x1)
12. x_x1_y
⊢ Colinear(x1;a;b)
BY
{ ((All (RWO "not-lsep-iff-colinear<") THENA Auto) THEN ParallelOp -2 THEN EAuto 2) }

---

Latex:

---

Latex:

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


By

---

Latex:
((All  (RWO  "not-lsep-iff-colinear<")  THENA  Auto)  THEN  ParallelOp  -2  THEN  EAuto  2)

---

Home Index