---

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


1. eu : EuclideanParPlane
2. L : LINE
3. M : LINE
4. l : {l:Line| l = L ∈ LINE} 
5. m : {m:Line| m = M ∈ LINE} 
6. l \/ m
7. l = L ∈ LINE
8. m = M ∈ LINE
9. 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))
10. a : Point
11. b : Point
12. Colinear(a;fst(l);fst(snd(l)))
13. Colinear(b;fst(l);fst(snd(l)))
14. a leftof fst(m)fst(snd(m))
15. b leftof fst(snd(m))fst(m)
⊢ ∃a,b:{c:Point| c I l} . (a leftof fst(m)fst(snd(m)) ∧ b leftof fst(snd(m))fst(m))
BY
{ ((InstConcl [⌜a⌝;⌜b⌝]⋅ THEN Auto)
   THEN (InstLemma  `geo-incident-line` [⌜eu⌝;⌜a⌝;⌜l⌝]⋅ THENA Auto)
   THEN (InstLemma  `geo-incident-line` [⌜eu⌝;⌜b⌝;⌜l⌝]⋅ THENA Auto)
   THEN D -2
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma    `geo-incident-line`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma    `geo-incident-line`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  D  -1
  THEN  Auto)

---

Home Index