---

Step * 1 1 1 1 1 2 of Lemma geo-intersect-lines-iff

.....antecedent..... 
1. e : EuclideanPlane
2. p : Line
3. x : Point
4. y : Point
5. l2 : x ≠ y
6. a : Point
7. b : Point
8. c : Point
9. d : Point
10. v : Point
11. a-v-b
12. c-v-d
13. a I p
14. b I p
15. c I <x, y, l2>
16. d I <x, y, l2>
17. a leftof cd
18. b leftof dc
19. c leftof ba
20. d leftof ab
21. Colinear(a;fst(p);fst(snd(p)))
22. a # cd
⊢ Colinear(c;d;y)
BY
{ (∀h:hyp. ((RWO "geo-incident-line" h THENA Auto) THEN Reduce h)  THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane
2.  p  :  Line
3.  x  :  Point
4.  y  :  Point
5.  l2  :  x  \mneq{}  y
6.  a  :  Point
7.  b  :  Point
8.  c  :  Point
9.  d  :  Point
10.  v  :  Point
11.  a-v-b
12.  c-v-d
13.  a  I  p
14.  b  I  p
15.  c  I  <x,  y,  l2>
16.  d  I  <x,  y,  l2>
17.  a  leftof  cd
18.  b  leftof  dc
19.  c  leftof  ba
20.  d  leftof  ab
21.  Colinear(a;fst(p);fst(snd(p)))
22.  a  \#  cd
\mvdash{}  Colinear(c;d;y)


By

---

Latex:
(\mforall{}h:hyp.  ((RWO  "geo-incident-line"  h  THENA  Auto)  THEN  Reduce  h)    THEN  Auto)

---

Home Index