---

Step * 2 1 1 1 1 1 2 1 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. y : Point
5. y2 : x1 ≠ y
6. z : Point
7. p : Point
8. Colinear(p;z;x)
9. Colinear(x1;y;p)
10. Colinear(p;z;p)
11. ∀u,v:Point.  (Colinear(x1;y;u) ⇒ Colinear(p;z;v) ⇒ Rupv)
12. z # x1y
13. z ≠ x
14. l : Line
15. x ≡ fst(l)
16. z ≡ fst(snd(l))
17. geo-line-sep(e;l;<x1, y, y2>)
⊢ Colinear(p;fst(l);fst(snd(l)))
BY
{ (RWO "-3< -2<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  y  :  Point
5.  y2  :  x1  \mneq{}  y
6.  z  :  Point
7.  p  :  Point
8.  Colinear(p;z;x)
9.  Colinear(x1;y;p)
10.  Colinear(p;z;p)
11.  \mforall{}u,v:Point.    (Colinear(x1;y;u)  {}\mRightarrow{}  Colinear(p;z;v)  {}\mRightarrow{}  Rupv)
12.  z  \#  x1y
13.  z  \mneq{}  x
14.  l  :  Line
15.  x  \mequiv{}  fst(l)
16.  z  \mequiv{}  fst(snd(l))
17.  geo-line-sep(e;l;<x1,  y,  y2>)
\mvdash{}  Colinear(p;fst(l);fst(snd(l)))


By

---

Latex:
(RWO  "-3<  -2<"  0  THEN  Auto)

---

Home Index