---

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


1. eu : EuclideanParPlane
2. L : LINE
3. M : LINE
4. L \/ M
⊢ ∃l:{l:Line| l = L ∈ LINE} . ∃m:{m:Line| m = M ∈ LINE} . l \/ m
BY
{ ((Unfold `geo-intersect` -1 THEN ExRepD)
   THEN (InstConcl [⌜l⌝;⌜m⌝]⋅ THEN Auto)
   THEN InstLemma `geo-intersect-lines` [⌜eu⌝;⌜l⌝;⌜m⌝]⋅
   THEN Auto) }

1
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

---

Latex:

---

Latex:

1.  eu  :  EuclideanParPlane
2.  L  :  LINE
3.  M  :  LINE
4.  L  \mbackslash{}/  M
\mvdash{}  \mexists{}l:\{l:Line|  l  =  L\}  .  \mexists{}m:\{m:Line|  m  =  M\}  .  l  \mbackslash{}/  m


By

---

Latex:
((Unfold  `geo-intersect`  -1  THEN  ExRepD)
  THEN  (InstConcl  [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-intersect-lines`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index