---

Step * 2 of Lemma geo-intersect-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)
⊢ 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
⊢ 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)
\mvdash{}  P  \mbackslash{}/  L


By

---

Latex:
ExRepD

---

Home Index