---

Step * 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)))
⊢ y \/ y1
BY
{ ((InstHyp [⌜y1⌝;⌜x⌝;⌜y⌝] (-1)⋅ THEN Auto) THEN D -1 THEN Auto) }

1
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. y1 \/ y
⊢ y \/ y1

2
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

---

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)))
\mvdash{}  y  \mbackslash{}/  y1


By

---

Latex:
((InstHyp  [\mkleeneopen{}y1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index