---

Step * 2 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. Sym(Point + Line;p,q.¬proj-point-sep(e;p;q))
4. a : Point + Line
5. b : Point + Line
6. c : Point + Line
7. ¬proj-point-sep(e;a;b)
8. ¬proj-point-sep(e;b;c)
9. proj-point-sep(e;a;c)
10. proj-point-sep(e;c;b)
⊢ False
BY
{ (D -3 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.  Sym(Point  +  Line;p,q.\mneg{}proj-point-sep(e;p;q))
4.  a  :  Point  +  Line
5.  b  :  Point  +  Line
6.  c  :  Point  +  Line
7.  \mneg{}proj-point-sep(e;a;b)
8.  \mneg{}proj-point-sep(e;b;c)
9.  proj-point-sep(e;a;c)
10.  proj-point-sep(e;c;b)
\mvdash{}  False


By

---

Latex:
(D  -3  THEN  EAuto  1)

---

Home Index