---

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


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. p \/ l
⊢ ∃x:Point. (x I p ∧ x I l)
BY
{ ((RWO "geo-intersect-iff2" (-1) THENA Auto) THEN ExRepD THEN Auto) }

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
⊢ ∃x:Point. (x I p ∧ x I l)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  p  \mbackslash{}/  l
\mvdash{}  \mexists{}x:Point.  (x  I  p  \mwedge{}  x  I  l)


By

---

Latex:
((RWO  "geo-intersect-iff2"  (-1)  THENA  Auto)  THEN  ExRepD  THEN  Auto)

---

Home Index