---

Step * of Lemma Euclid-Prop31

No Annotations
∀e:EuclideanPlane. ∀a,b,x:Point.  (a # b ⇒ x # ab ⇒ (∃y:Point. geo-parallel-points(e;a;b;x;y)))
BY
{ (Auto
   THEN (InstLemma `Euclid-drop-perp-0` [⌜e⌝;⌜a⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `z' (-2)
   THEN D -1
   THEN RenameVar `u' (-2)
   THEN (InstLemma `Euclid-erect-perp` [⌜e⌝;⌜z⌝;⌜x⌝;⌜x⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `q' (-2)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. [%9] : Colinear(u;z;x) ∧ ab  ⊥u uz ∧ z # ab ∧ z # x
10. q : Point
11. [%16] : zx  ⊥x qx ∧ q # zx
⊢ ∃y:Point. geo-parallel-points(e;a;b;x;y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x:Point.    (a  \#  b  {}\mRightarrow{}  x  \#  ab  {}\mRightarrow{}  (\mexists{}y:Point.  geo-parallel-points(e;a;b;x;y)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-drop-perp-0`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\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{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `q'  (-2))

---

Home Index