---

Step * 2 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)
⊢ ¬proj-point-sep(e;a;c)
BY
{ ((D 0 THENA Auto) THEN (InstLemma `proj-point-sep-cotrans` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝]⋅ THENA Auto) THEN D -1 THEN Auto) }

1
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

---

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)
\mvdash{}  \mneg{}proj-point-sep(e;a;c)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `proj-point-sep-cotrans`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index