---

Step * 2 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. x : Point
3. y : Line
4. True
⊢ ∃n:Line?. ((¬pp-sep(e;inl x;n)) ∧ pp-sep(e;inr y ;n))
BY
{ Assert ⌜∃m:Line. (y \/ m ∧ x I m)⌝⋅ }

1
.....assertion..... 
1. e : EuclideanParPlane
2. x : Point
3. y : Line
4. True
⊢ ∃m:Line. (y \/ m ∧ x I m)

2
1. e : EuclideanParPlane
2. x : Point
3. y : Line
4. True
5. ∃m:Line. (y \/ m ∧ x I m)
⊢ ∃n:Line?. ((¬pp-sep(e;inl x;n)) ∧ pp-sep(e;inr y ;n))

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  y  :  Line
4.  True
\mvdash{}  \mexists{}n:Line?.  ((\mneg{}pp-sep(e;inl  x;n))  \mwedge{}  pp-sep(e;inr  y  ;n))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}m:Line.  (y  \mbackslash{}/  m  \mwedge{}  x  I  m)\mkleeneclose{}\mcdot{}

---

Home Index