---

Step * 1 of Lemma not-proj-point-sep-is-equiv


1. e : EuclideanParPlane
2. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
3. a : Point + Line
4. b : Point + Line
5. ¬proj-point-sep(e;a;b)
⊢ ¬proj-point-sep(e;b;a)
BY
{ (ParallelLast THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  \mforall{}l,m:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:Line.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))
3.  a  :  Point  +  Line
4.  b  :  Point  +  Line
5.  \mneg{}proj-point-sep(e;a;b)
\mvdash{}  \mneg{}proj-point-sep(e;b;a)


By

---

Latex:
(ParallelLast  THEN  EAuto  1)

---

Home Index