---

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

∀e:EuclideanParPlane
  ((∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))) ⇒ EquivRel(Point + Line;p,q.¬proj-point-sep(e;p;q)))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
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)

2
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)

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane
    ((\mforall{}l,m:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:Line.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))))
    {}\mRightarrow{}  EquivRel(Point  +  Line;p,q.\mneg{}proj-point-sep(e;p;q)))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index