---

Step * 1 1 1 2 4 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(z;fst(snd(l));x)
BY
{ (((InstLemma `geo-incident-line` [⌜eu⌝;⌜z⌝;⌜l⌝]⋅ THEN Auto)
    THEN InstLemma `geo-incident-line` [⌜eu⌝;⌜x⌝;⌜l⌝]⋅
    THEN Auto)
   THEN InstLemma `geo-colinear-transitivity` [⌜eu⌝;⌜z⌝;⌜fst(l)⌝;⌜fst(snd(l))⌝;⌜x⌝]⋅
   THEN EAuto 2) }

---

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(z;fst(snd(l));x)


By

---

Latex:
(((InstLemma  `geo-incident-line`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Auto)
    THEN  InstLemma  `geo-incident-line`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  InstLemma  `geo-colinear-transitivity`  [\mkleeneopen{}eu\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}fst(l)\mkleeneclose{};\mkleeneopen{}fst(snd(l))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  EAuto  2)

---

Home Index