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