---

Step * of Lemma geo-intersect-lines-iff

∀e:EuclideanPlane. ∀p,l:Line.  (p \/ l ⇐⇒ geo-line-sep(e;p;l) ∧ (∃x:Point. (x I p ∧ x I l)))
BY
{ Auto }

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

2
1. e : EuclideanPlane
2. p : Line
3. l : Line
4. p \/ l
⊢ ∃x:Point. (x I p ∧ x I l)

3
1. e : EuclideanPlane
2. p : Line
3. l : Line
4. geo-line-sep(e;p;l)
5. ∃x:Point. (x I p ∧ x I l)
⊢ p \/ l

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}p,l:Line.    (p  \mbackslash{}/  l  \mLeftarrow{}{}\mRightarrow{}  geo-line-sep(e;p;l)  \mwedge{}  (\mexists{}x:Point.  (x  I  p  \mwedge{}  x  I  l)))


By

---

Latex:
Auto

---

Home Index