---

Step * 2 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
⊢ ∃a,b:{c:Point| c I l} . (a leftof fst(m)fst(snd(m)) ∧ b leftof fst(snd(m))fst(m))
BY
{ ((InstLemma `geo-intersect-lines` [⌜eu⌝;⌜l⌝;⌜m⌝]⋅ THEN Auto) THEN D -1 THEN D -1) }

1
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)))
∧ Colinear(b;fst(l);fst(snd(l)))
∧ a leftof fst(m)fst(snd(m))
∧ 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))

---

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
\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:
((InstLemma  `geo-intersect-lines`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  D  -1)

---

Home Index