---

Step * 1 1 of Lemma geo-intersect-unique


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. (z I l ∧ z # m)
⊢ x ≡ y
BY
{ (InstLemma `geo-intersection-unicity` [⌜eu⌝]⋅ THENA Auto) }

1
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. (z I l ∧ z # m)
12. ∀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)
⊢ x ≡ y

---

Latex:

---

Latex:

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.  \mexists{}z:Point.  (z  I  l  \mwedge{}  z  \#  m)
\mvdash{}  x  \mequiv{}  y


By

---

Latex:
(InstLemma  `geo-intersection-unicity`  [\mkleeneopen{}eu\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index