Step
*
of Lemma
geo-congruent-flip2
No Annotations
∀e:EuclideanPlane. ∀[a,b:Point].  ab ≅ ba
BY
{ ((Auto THEN D 1) THEN Unhide THEN EAuto 1) }
Latex:
Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    ab  \mcong{}  ba
By
Latex:
((Auto  THEN  D  1)  THEN  Unhide  THEN  EAuto  1)
Home
Index