---

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


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

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
⊢ ∃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.  \mexists{}l:\{l:Line|  l  =  L\}  .  \mexists{}m:\{m:Line|  m  =  M\}  .  l  \mbackslash{}/  m
\mvdash{}  L  \mbackslash{}/  M


By

---

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

---

Home Index