---

Step * 1 1 1 of Lemma geo-tar-same-side-iff


1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. c : Point
7. P # AB
8. c # AB
9. t1 : Point
10. Colinear(A;B;t1)
11. B(Pt1c)
12. Q # AB
13. c # AB
14. t : Point
15. Colinear(A;B;t)
16. B(Qtc)
17. Q leftof BA
18. P leftof AB
⊢ Q leftof AB
BY
{ ((All (RWO "not-lsep-iff-colinear<") THENA Auto)
   THEN D 8
   THEN Try (((Assert t1 leftof AB BY EasyGeometry) THEN D 10 THEN Auto))) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. c : Point
7. P # AB
8. c leftof BA
9. t1 : Point
10. ¬A # Bt1
11. B(Pt1c)
12. Q # AB
13. c # AB
14. t : Point
15. ¬A # Bt
16. B(Qtc)
17. Q leftof BA
18. P leftof AB
⊢ Q leftof AB

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  P  :  Point
5.  Q  :  Point
6.  c  :  Point
7.  P  \#  AB
8.  c  \#  AB
9.  t1  :  Point
10.  Colinear(A;B;t1)
11.  B(Pt1c)
12.  Q  \#  AB
13.  c  \#  AB
14.  t  :  Point
15.  Colinear(A;B;t)
16.  B(Qtc)
17.  Q  leftof  BA
18.  P  leftof  AB
\mvdash{}  Q  leftof  AB


By

---

Latex:
((All  (RWO  "not-lsep-iff-colinear<")  THENA  Auto)
  THEN  D  8
  THEN  Try  (((Assert  t1  leftof  AB  BY  EasyGeometry)  THEN  D  10  THEN  Auto)))

---

Home Index