---

Step * 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. P # AB
18. Q # AB
19. P leftof AB
⊢ Q leftof AB
BY
{ (Thin (-3) THEN D -2 THEN Try (Trivial)) }

1
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

---

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.  P  leftof  AB
\mvdash{}  Q  leftof  AB


By

---

Latex:
(Thin  (-3)  THEN  D  -2  THEN  Try  (Trivial))

---

Home Index