---

Step * of Lemma geo-intersect-lines

No Annotations
∀e:EuclideanPlane. ∀p,l:Line.
  (p \/ l
  ⇐⇒ ∃a,b:Point
       (Colinear(a;fst(p);fst(snd(p)))
       ∧ Colinear(b;fst(p);fst(snd(p)))
       ∧ a leftof fst(l)fst(snd(l))
       ∧ b leftof fst(snd(l))fst(l)))
BY
{ Auto }

1
1. e : EuclideanPlane
2. p : Line
3. l : Line
4. p \/ l
⊢ ∃a,b:Point
   (Colinear(a;fst(p);fst(snd(p)))
   ∧ Colinear(b;fst(p);fst(snd(p)))
   ∧ a leftof fst(l)fst(snd(l))
   ∧ b leftof fst(snd(l))fst(l))

2
1. e : EuclideanPlane
2. p : Line
3. l : Line
4. ∃a,b:Point
    (Colinear(a;fst(p);fst(snd(p)))
    ∧ Colinear(b;fst(p);fst(snd(p)))
    ∧ a leftof fst(l)fst(snd(l))
    ∧ b leftof fst(snd(l))fst(l))
⊢ p \/ l

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}p,l:Line.
    (p  \mbackslash{}/  l
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}a,b:Point
              (Colinear(a;fst(p);fst(snd(p)))
              \mwedge{}  Colinear(b;fst(p);fst(snd(p)))
              \mwedge{}  a  leftof  fst(l)fst(snd(l))
              \mwedge{}  b  leftof  fst(snd(l))fst(l)))


By

---

Latex:
Auto

---

Home Index