---

Step * 1 2 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. P # AB
18. Q # AB
19. Q leftof AB
⊢ P leftof AB
BY
{ (Thin (-2)
   THEN D -2
   THEN Try (Trivial)
   THEN (All (RWO "not-lsep-iff-colinear<") THENA Auto)
   THEN D 8
   THEN Try (((Assert t1 leftof BA 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 AB
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. P leftof BA
18. Q leftof AB
⊢ P 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.  P  \#  AB
18.  Q  \#  AB
19.  Q  leftof  AB
\mvdash{}  P  leftof  AB


By

---

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

---

Home Index