---

Step * of Lemma geo-extend-exists1

∀e:BasicGeometry. ∀q,a,b,c:Point.  (q ≠ a ⇒ (∃x:Point. ((b ≠ c ⇒ q-a-x) ∧ ax ≅ bc)))
BY
{ (Auto THEN RenameVar `sqa' (-1) THEN InstLemma  `geo-extend-property1` [⌜e⌝;⌜q⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜sqa⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}q,a,b,c:Point.    (q  \mneq{}  a  {}\mRightarrow{}  (\mexists{}x:Point.  ((b  \mneq{}  c  {}\mRightarrow{}  q-a-x)  \mwedge{}  ax  \00D0  bc)))


By

---

Latex:
(Auto
  THEN  RenameVar  `sqa'  (-1)
  THEN  InstLemma    `geo-extend-property1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}sqa\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index