---

Step * of Lemma geo-Aparallel-trans-lines

∀e:EuclideanParPlane. ∀l,m,n:Line.  (l || m ⇒ m || n ⇒ l || n)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "geo-intersect-iff2" (-1) THENA Auto)
   THEN ExRepD
   THEN (InstLemma `geo-playfair-axiom` [⌜e⌝;⌜v⌝;⌜m⌝;⌜l⌝;⌜n⌝]⋅
         THENA (Auto THEN Try ((BLemma `geo-Aparallel_sym` THEN Auto)))
         )) }

1
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

2
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 n

3
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

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}l,m,n:Line.    (l  ||  m  {}\mRightarrow{}  m  ||  n  {}\mRightarrow{}  l  ||  n)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (RWO  "geo-intersect-iff2"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `geo-playfair-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((BLemma  `geo-Aparallel\_sym`  THEN  Auto)))
              ))

---

Home Index