---

Step * 1 of Lemma proj-point-sep_defB


1. e : EuclideanParPlane
2. x1 : Point
3. x2 : Point
4. x : Line
5. ¬x1 # x
6. x2 # x
7. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
⊢ x1 ≠ x2
BY
{ (GetLinePoints 4 THEN All (RepUR ``geo-plsep``)) }

1
1. e : EuclideanParPlane
2. x1 : Point
3. x2 : Point
4. x3 : Point
5. y : Point
6. x5 : x3 ≠ y
7. ¬x1 # x3y
8. x2 # x3y
9. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
⊢ x1 ≠ x2

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x1  :  Point
3.  x2  :  Point
4.  x  :  Line
5.  \mneg{}x1  \#  x
6.  x2  \#  x
7.  \mforall{}l,m:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:Line.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))
\mvdash{}  x1  \mneq{}  x2


By

---

Latex:
(GetLinePoints  4  THEN  All  (RepUR  ``geo-plsep``))

---

Home Index