---

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


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. ∃a,b,c,d,v:Point
    (a-v-b ∧ c-v-d ∧ a I p ∧ b I p ∧ c I l ∧ d I l ∧ a leftof cd ∧ b leftof dc ∧ c leftof ba ∧ d leftof ab)
⊢ geo-line-sep(e;p;l)
BY
{ ExRepD }

1
1. e : EuclideanPlane
2. p : Line
3. l : Line
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I p
12. b I p
13. c I l
14. d I l
15. a leftof cd
16. b leftof dc
17. c leftof ba
18. d leftof ab
⊢ geo-line-sep(e;p;l)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  \mexists{}a,b,c,d,v:Point
        (a-v-b
        \mwedge{}  c-v-d
        \mwedge{}  a  I  p
        \mwedge{}  b  I  p
        \mwedge{}  c  I  l
        \mwedge{}  d  I  l
        \mwedge{}  a  leftof  cd
        \mwedge{}  b  leftof  dc
        \mwedge{}  c  leftof  ba
        \mwedge{}  d  leftof  ab)
\mvdash{}  geo-line-sep(e;p;l)


By

---

Latex:
ExRepD

---

Home Index