---

Step * 1 1 of Lemma geo-intersect-LINE-iff-line


1. eu : EuclideanParPlane
2. L : LINE
3. M : LINE
4. l : Line
5. m : Line
6. l = L ∈ LINE
7. m = M ∈ LINE
8. a : {a:Point| a I l} 
9. b : {c:Point| c I l} 
10. a leftof fst(m)fst(snd(m))
11. b leftof fst(snd(m))fst(m)
12. l \/ m
⇒ (∃a,b:Point
     (Colinear(a;fst(l);fst(snd(l)))
     ∧ Colinear(b;fst(l);fst(snd(l)))
     ∧ a leftof fst(m)fst(snd(m))
     ∧ b leftof fst(snd(m))fst(m)))
13. l \/ m ⇐ ∃a,b:Point
               (Colinear(a;fst(l);fst(snd(l)))
               ∧ Colinear(b;fst(l);fst(snd(l)))
               ∧ a leftof fst(m)fst(snd(m))
               ∧ b leftof fst(snd(m))fst(m))
⊢ l \/ m
BY
{ (D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  eu  :  EuclideanParPlane
2.  L  :  LINE
3.  M  :  LINE
4.  l  :  Line
5.  m  :  Line
6.  l  =  L
7.  m  =  M
8.  a  :  \{a:Point|  a  I  l\} 
9.  b  :  \{c:Point|  c  I  l\} 
10.  a  leftof  fst(m)fst(snd(m))
11.  b  leftof  fst(snd(m))fst(m)
12.  l  \mbackslash{}/  m
{}\mRightarrow{}  (\mexists{}a,b:Point
          (Colinear(a;fst(l);fst(snd(l)))
          \mwedge{}  Colinear(b;fst(l);fst(snd(l)))
          \mwedge{}  a  leftof  fst(m)fst(snd(m))
          \mwedge{}  b  leftof  fst(snd(m))fst(m)))
13.  l  \mbackslash{}/  m  \mLeftarrow{}{}  \mexists{}a,b:Point
                              (Colinear(a;fst(l);fst(snd(l)))
                              \mwedge{}  Colinear(b;fst(l);fst(snd(l)))
                              \mwedge{}  a  leftof  fst(m)fst(snd(m))
                              \mwedge{}  b  leftof  fst(snd(m))fst(m))
\mvdash{}  l  \mbackslash{}/  m


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index