Step
*
of Lemma
sq_stable__midpoint
∀e:EuclideanPlaneStructure. ∀[a,b,c:Point].  SqStable(a=c=b)
BY
{ (Auto THEN Unfold `geo-midpoint` 0 THEN Auto) }
Latex:
Latex:
\mforall{}e:EuclideanPlaneStructure.  \mforall{}[a,b,c:Point].    SqStable(a=c=b)
By
Latex:
(Auto  THEN  Unfold  `geo-midpoint`  0  THEN  Auto)
Home
Index