---

Step * of Lemma Euclid-parallel-exists

∀e:EuclideanPlane. ∀l:Line. ∀p:Point.  ∃m:Line. (m || l ∧ p I m)
BY
{ ((Auto THEN GetLinePoints (2))
   THEN (InstLemma `Euclid-drop-perp-0` [⌜e⌝;⌜x⌝;⌜y⌝;⌜p⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `z' (-2)
   THEN D -1
   THEN RenameVar `u' (-2)
   THEN (InstLemma `Euclid-erect-perp` [⌜e⌝;⌜z⌝;⌜p⌝;⌜p⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `q' (-2)) }

1
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. p : Point
6. z : Point
7. u : Point
8. [%3] : Colinear(u;z;p) ∧ xy  ⊥u uz ∧ z # xy ∧ z ≠ p
9. q : Point
10. [%5] : zp  ⊥p qp ∧ q # zp
⊢ ∃m:Line. (m || <x, y, l2> ∧ p I m)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}l:Line.  \mforall{}p:Point.    \mexists{}m:Line.  (m  ||  l  \mwedge{}  p  I  m)


By

---

Latex:
((Auto  THEN  GetLinePoints  (2))
  THEN  (InstLemma  `Euclid-drop-perp-0`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `z'  (-2)
  THEN  D  -1
  THEN  RenameVar  `u'  (-2)
  THEN  (InstLemma  `Euclid-erect-perp`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `q'  (-2))

---

Home Index