---

Step * 3 1 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 ab
8. x leftof ab ⇒ y leftof ba
9. x leftof ab ⇐ y leftof ba
10. x1 : Point
11. Colinear(b;a;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  ba
7.  y  leftof  ab
8.  x  leftof  ab  {}\mRightarrow{}  y  leftof  ba
9.  x  leftof  ab  \mLeftarrow{}{}  y  leftof  ba
10.  x1  :  Point
11.  Colinear(b;a;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