---

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


1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. y : Point
5. y2 : x1 ≠ y
⊢ ∃m:Line. (<x1, y, y2> \/ m ∧ x I m)
BY
{ ((InstLemma `Euclid-drop-perp-00` [⌜e⌝;⌜x1⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto) THEN RepeatFor 2 (D -1) THEN RenameVar `z' (-3)) }

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) ∧ x1y  ⊥p pz ∧ z # x1y ∧ z ≠ x
⊢ ∃m:Line. (<x1, y, y2> \/ m ∧ x I m)

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  y  :  Point
5.  y2  :  x1  \mneq{}  y
\mvdash{}  \mexists{}m:Line.  (<x1,  y,  y2>  \mbackslash{}/  m  \mwedge{}  x  I  m)


By

---

Latex:
((InstLemma  `Euclid-drop-perp-00`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  RenameVar  `z'  (-3))

---

Home Index