---

Step * 1 of Lemma geo-intersect-lines


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. p \/ l
⊢ ∃a,b:Point
   (Colinear(a;fst(p);fst(snd(p)))
   ∧ Colinear(b;fst(p);fst(snd(p)))
   ∧ a leftof fst(l)fst(snd(l))
   ∧ b leftof fst(snd(l))fst(l))
BY
{ (RWO "geo-intersect-iff2" (-1) THEN Auto THEN ExRepD THEN GetLinePoints (3) THEN GetLinePoints (2)) }

1
1. e : EuclideanPlane
2. x1 : Point
3. y1 : Point
4. p2 : x1 # y1
5. x : Point
6. y : Point
7. l2 : x # y
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 <x1, y1, p2>
16. b I <x1, y1, p2>
17. c I <x, y, l2>
18. d I <x, y, l2>
19. a leftof cd
20. b leftof dc
21. c leftof ba
22. d leftof ab
⊢ ∃a,b:Point. (Colinear(a;x1;y1) ∧ Colinear(b;x1;y1) ∧ a leftof xy ∧ b leftof yx)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  p  \mbackslash{}/  l
\mvdash{}  \mexists{}a,b:Point
      (Colinear(a;fst(p);fst(snd(p)))
      \mwedge{}  Colinear(b;fst(p);fst(snd(p)))
      \mwedge{}  a  leftof  fst(l)fst(snd(l))
      \mwedge{}  b  leftof  fst(snd(l))fst(l))


By

---

Latex:
(RWO  "geo-intersect-iff2"  (-1)  THEN  Auto  THEN  ExRepD  THEN  GetLinePoints  (3)  THEN  GetLinePoints  (2))

---

Home Index