---

Step * 1 1 1 2 3 of Lemma geo-intersect-unique

.....antecedent..... 
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
      ((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(snd(l)) ≠ z
⊢ Colinear(fst(m);fst(snd(m));y)
BY
{ (InstLemma `geo-incident-line` [⌜eu⌝;⌜y⌝;⌜m⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  eu  :  EuclideanParPlane@i'
2.  l  :  Line@i
3.  m  :  Line@i
4.  x  :  Point@i
5.  y  :  Point@i
6.  l  \mbackslash{}/  m
7.  x  I  l
8.  x  I  m
9.  y  I  l
10.  y  I  m
11.  z  :  Point
12.  z  I  l
13.  z  \#  m
14.  \mforall{}a,b,c,d,p,q:Point.
            ((\mneg{}Colinear(a;b;c))
            {}\mRightarrow{}  c  \mneq{}  d
            {}\mRightarrow{}  Colinear(a;b;p)
            {}\mRightarrow{}  Colinear(a;b;q)
            {}\mRightarrow{}  Colinear(c;d;p)
            {}\mRightarrow{}  Colinear(c;d;q)
            {}\mRightarrow{}  p  \mequiv{}  q)
15.  fst(snd(l))  \mneq{}  z
\mvdash{}  Colinear(fst(m);fst(snd(m));y)


By

---

Latex:
(InstLemma  `geo-incident-line`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index