---

Step * 1 of Lemma Mid_perm


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. B=A=C
6. B=A=C
⊢ C=A=B
BY
{ (((Auto THEN InstLemma `geo-midpoint-symmetry` [⌜e⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅) THENA Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  B=A=C
6.  B=A=C
\mvdash{}  C=A=B


By

---

Latex:
(((Auto  THEN  InstLemma  `geo-midpoint-symmetry`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{})  THENA  Auto)  THEN  Auto)

---

Home Index