---

Step * of Lemma circle-circle-continuity1

∀e:EuclideanPlane. ∀a,b,c,d:Point.
  ((¬(a = c ∈ Point))
  ⇒ (∃p,q,x,z:Point. (a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd))
  ⇒ (∃y:Point. (ay=ab ∧ cy=cd)))
BY
{ (Auto THEN ExRepD THEN InstLemma `circle-circle-continuity`  [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜p⌝;⌜q⌝;⌜x⌝;⌜z⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    ((\mneg{}(a  =  c))
    {}\mRightarrow{}  (\mexists{}p,q,x,z:Point.  (a\_x\_b  \mwedge{}  a\_b\_z  \mwedge{}  ap=ax  \mwedge{}  aq=az  \mwedge{}  cp=cd  \mwedge{}  cq=cd))
    {}\mRightarrow{}  (\mexists{}y:Point.  (ay=ab  \mwedge{}  cy=cd)))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  InstLemma  `circle-circle-continuity` 
  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index