---

Step * of Lemma geo-intersect-unique

∀eu:EuclideanParPlane. ∀l,m:Line. ∀x,y:Point.  (l \/ m ⇒ (x I l ∧ x I m) ⇒ (y I l ∧ y I m) ⇒ x ≡ y)
BY
{ 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
⊢ x ≡ y

---

Latex:

---

Latex:
\mforall{}eu:EuclideanParPlane.  \mforall{}l,m:Line.  \mforall{}x,y:Point.
    (l  \mbackslash{}/  m  {}\mRightarrow{}  (x  I  l  \mwedge{}  x  I  m)  {}\mRightarrow{}  (y  I  l  \mwedge{}  y  I  m)  {}\mRightarrow{}  x  \mequiv{}  y)


By

---

Latex:
Auto

---

Home Index