---

Step * 2 1 1 1 1 2 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) ∧ x1y  ⊥p pz ∧ z # x1y ∧ z ≠ x
9. l : Line
10. x ≡ fst(l) ∧ z ≡ fst(snd(l))
⊢ x I l
BY
{ (((RWO "geo-incident-line" 0 THENA Auto) THEN D -1) THEN RWO "-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)  \mwedge{}  x1y    \mbot{}p  pz  \mwedge{}  z  \#  x1y  \mwedge{}  z  \mneq{}  x
9.  l  :  Line
10.  x  \mequiv{}  fst(l)  \mwedge{}  z  \mequiv{}  fst(snd(l))
\mvdash{}  x  I  l


By

---

Latex:
(((RWO  "geo-incident-line"  0  THENA  Auto)  THEN  D  -1)  THEN  RWO  "-2<"  0  THEN  Auto)

---

Home Index