---

Step * of Lemma geo-perp-midsegments

No Annotations
∀e:BasicGeometry. ∀a,b,c:Point.  (Rabc ⇒ (∀c',d,p:Point.  (c'=p=d ⇒ c'=a=c ⇒ d=b=c ⇒ Rbap)))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Rabc
6. c' : Point
7. d : Point
8. p : Point
9. c'=p=d
10. c'=a=c
11. d=b=c
⊢ Rbap

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (Rabc  {}\mRightarrow{}  (\mforall{}c',d,p:Point.    (c'=p=d  {}\mRightarrow{}  c'=a=c  {}\mRightarrow{}  d=b=c  {}\mRightarrow{}  Rbap)))


By

---

Latex:
Auto

---

Home Index