---

Step * 3 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
23. l ≡ n
⊢ False
BY
{ ((Assert l = n ∈ LINE BY (EqTypeCD THEN Auto)) THEN (Assert ¬n \/ n BY Auto) THEN D -1 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
23.  l  \mequiv{}  n
\mvdash{}  False


By

---

Latex:
((Assert  l  =  n  BY  (EqTypeCD  THEN  Auto))  THEN  (Assert  \mneg{}n  \mbackslash{}/  n  BY  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index