---

Step * 2 1 of Lemma proj-point-sep_defA

.....assertion..... 
1. e : EuclideanParPlane
2. x : Point
3. y : Line
4. True
⊢ ∃m:Line. (y \/ m ∧ x I m)
BY
{ (Thin (-1) THEN GetLinePoints (-1)) }

1
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. y : Point
5. y2 : x1 ≠ y
⊢ ∃m:Line. (<x1, y, y2> \/ m ∧ x I m)

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  y  :  Line
4.  True
\mvdash{}  \mexists{}m:Line.  (y  \mbackslash{}/  m  \mwedge{}  x  I  m)


By

---

Latex:
(Thin  (-1)  THEN  GetLinePoints  (-1))

---

Home Index