---

Step * of Lemma Euclid-parallel-points-exists

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀p:Point.  ∃q:Point. geo-parallel-points(e;a;b;p;q)
BY
{ (Auto
   THEN (InstLemma `Euclid-drop-perp-0` [⌜e⌝;⌜a⌝;⌜b⌝;⌜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. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. [%3] : Colinear(u;z;p) ∧ ab  ⊥u uz ∧ z # ab ∧ z # p
8. q : Point
9. [%5] : zp  ⊥p qp ∧ q # zp
⊢ ∃q:Point. geo-parallel-points(e;a;b;p;q)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}p:Point.
    \mexists{}q:Point.  geo-parallel-points(e;a;b;p;q)


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-drop-perp-0`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\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