---

Step * 1 2 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 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
BY
{ (D -6 THEN Try (((Assert t leftof AB BY EasyGeometry) THEN D 15 THEN Auto))) }

---

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  leftof  AB
9.  t1  :  Point
10.  \mneg{}A  \#  Bt1
11.  B(Pt1c)
12.  Q  \#  AB
13.  c  \#  AB
14.  t  :  Point
15.  \mneg{}A  \#  Bt
16.  B(Qtc)
17.  P  leftof  BA
18.  Q  leftof  AB
\mvdash{}  P  leftof  AB


By

---

Latex:
(D  -6  THEN  Try  (((Assert  t  leftof  AB  BY  EasyGeometry)  THEN  D  15  THEN  Auto)))

---

Home Index