---

Step * 1 1 1 1 1 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(l) ≠ z
⊢ ¬Colinear(fst(m);fst(snd(m));z)
BY
{ ((InstLemma `not-lsep-iff-colinear` [⌜eu⌝]⋅ THENA Auto)
   THEN Unfold `geo-plsep` -4
   THEN (InstHyp [⌜z⌝;⌜fst(m)⌝;⌜fst(snd(m))⌝] (-1)⋅ THEN Auto)
   THEN D 0) }

---

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(l)  \mneq{}  z
\mvdash{}  \mneg{}Colinear(fst(m);fst(snd(m));z)


By

---

Latex:
((InstLemma  `not-lsep-iff-colinear`  [\mkleeneopen{}eu\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `geo-plsep`  -4
  THEN  (InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}fst(m)\mkleeneclose{};\mkleeneopen{}fst(snd(m))\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  THEN  D  0)

---

Home Index