---

Step * 2 1 1 1 1 1 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. x1y  ⊥p pz
10. z # x1y
11. z ≠ x
12. l : Line
13. x ≡ fst(l)
14. z ≡ fst(snd(l))
⊢ geo-line-sep(e;l;<x1, y, y2>)
BY
{ (RepUR ``geo-line-sep`` 0 THEN (RWO "-1< -2<" 0 THENA Auto)) }

1
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. x1y  ⊥p pz
10. z # x1y
11. z ≠ x
12. l : Line
13. x ≡ fst(l)
14. z ≡ fst(snd(l))
⊢ ∃p:Point. (Colinear(p;x;z) ∧ p # x1y)

---

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.  x1y    \mbot{}p  pz
10.  z  \#  x1y
11.  z  \mneq{}  x
12.  l  :  Line
13.  x  \mequiv{}  fst(l)
14.  z  \mequiv{}  fst(snd(l))
\mvdash{}  geo-line-sep(e;l;<x1,  y,  y2>)


By

---

Latex:
(RepUR  ``geo-line-sep``  0  THEN  (RWO  "-1<  -2<"  0  THENA  Auto))

---

Home Index