---

Step * of Lemma geo-intersect-iff

∀e:EuclideanPlane. ∀P,L:LINE.
  (P \/ L ⇐⇒ ∃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))
BY
{ Auto }

1
1. e : EuclideanPlane
2. P : LINE
3. L : LINE
4. P \/ L
⊢ ∃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)

2
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

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}P,L:LINE.
    (P  \mbackslash{}/  L
    \mLeftarrow{}{}\mRightarrow{}  \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))


By

---

Latex:
Auto

---

Home Index