---

Step * of Lemma circle-circle-continuity2

∀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) ∧ (¬(x = z ∈ Point))))
  ⇒ (∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ (¬(z1 = z2 ∈ Point)))))
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)  \mwedge{}  (\mneg{}(x  =  z))))
    {}\mRightarrow{}  (\mexists{}z1,z2:Point.  (az1=ab  \mwedge{}  az2=ab  \mwedge{}  cz1=cd  \mwedge{}  cz2=cd  \mwedge{}  (\mneg{}(z1  =  z2)))))


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