---

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


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. p \/ l
⊢ geo-line-sep(e;p;l)
BY
{ (RWO "geo-intersect-iff2" (-1) THENA Auto) }

1
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)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  p  \mbackslash{}/  l
\mvdash{}  geo-line-sep(e;p;l)


By

---

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

---

Home Index