---

Step * 2 2 of Lemma proj-point-sep_defB


1. e : EuclideanParPlane
2. y : Line
3. y1 : Line
4. x : Line
5. ¬y \/ x
6. y1 \/ x
7. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
8. x \/ y
⊢ y \/ y1
BY
{ (D -4 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  y  :  Line
3.  y1  :  Line
4.  x  :  Line
5.  \mneg{}y  \mbackslash{}/  x
6.  y1  \mbackslash{}/  x
7.  \mforall{}l,m:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:Line.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))
8.  x  \mbackslash{}/  y
\mvdash{}  y  \mbackslash{}/  y1


By

---

Latex:
(D  -4  THEN  EAuto  1)

---

Home Index