---

Step * 1 of Lemma geo-intersect-iff2


1. e : EuclideanPlane
2. p : LINE
3. l : LINE
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I p
12. b I p
13. c I l
14. d I l
15. a leftof cd
16. b leftof dc
17. a-v-b
18. c-v-d
19. a I p
20. b I p
21. c I l
22. d I l
23. a leftof cd
24. b leftof dc
⊢ c leftof ba
BY
{ (D 18 THEN D 17 THEN (Assert c leftof bv BY EasyGeometry) THEN EasyGeometry) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  LINE
3.  l  :  LINE
4.  a  :  Point
5.  b  :  Point
6.  c  :  Point
7.  d  :  Point
8.  v  :  Point
9.  a-v-b
10.  c-v-d
11.  a  I  p
12.  b  I  p
13.  c  I  l
14.  d  I  l
15.  a  leftof  cd
16.  b  leftof  dc
17.  a-v-b
18.  c-v-d
19.  a  I  p
20.  b  I  p
21.  c  I  l
22.  d  I  l
23.  a  leftof  cd
24.  b  leftof  dc
\mvdash{}  c  leftof  ba


By

---

Latex:
(D  18  THEN  D  17  THEN  (Assert  c  leftof  bv  BY  EasyGeometry)  THEN  EasyGeometry)

---

Home Index