---

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


1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. geo-tar-same-side(e;P;Q;A;B)
⊢ P # AB ∧ Q # AB ∧ (P leftof AB ⇐⇒ Q leftof AB)
BY
{ (RepeatFor 2 (D -1) THEN (D -2 THEN D -1) THEN ExRepD 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 # 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

2
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

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  P  :  Point
5.  Q  :  Point
6.  geo-tar-same-side(e;P;Q;A;B)
\mvdash{}  P  \#  AB  \mwedge{}  Q  \#  AB  \mwedge{}  (P  leftof  AB  \mLeftarrow{}{}\mRightarrow{}  Q  leftof  AB)


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  (D  -2  THEN  D  -1)  THEN  ExRepD  THEN  Auto)

---

Home Index