---

Step * 1 of Lemma geo-Aparallel-trans-lines


1. e : EuclideanParPlane
2. l : Line
3. m : Line
4. n : Line
5. l || m
6. m || n
7. l \/ n
8. a : Point
9. b : Point
10. c : Point
11. d : Point
12. v : Point
13. a-v-b
14. c-v-d
15. a I l
16. b I l
17. c I n
18. d I n
19. a leftof cd
20. b leftof dc
21. c leftof ba
22. d leftof ab
⊢ v I l
BY
{ (FLemma `geo-strict-between-incident` [-10;-8] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  l  :  Line
3.  m  :  Line
4.  n  :  Line
5.  l  ||  m
6.  m  ||  n
7.  l  \mbackslash{}/  n
8.  a  :  Point
9.  b  :  Point
10.  c  :  Point
11.  d  :  Point
12.  v  :  Point
13.  a-v-b
14.  c-v-d
15.  a  I  l
16.  b  I  l
17.  c  I  n
18.  d  I  n
19.  a  leftof  cd
20.  b  leftof  dc
21.  c  leftof  ba
22.  d  leftof  ab
\mvdash{}  v  I  l


By

---

Latex:
(FLemma  `geo-strict-between-incident`  [-10;-8]  THEN  Auto)

---

Home Index