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