---

Step * of Lemma geo-be-compress

∀e:BasicGeometry. ∀a,b,c:Point.  (a_b_c ⇒ a_c_b ⇒ b ≡ c)
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. a_c_b
⊢ b ≡ c

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (a\_b\_c  {}\mRightarrow{}  a\_c\_b  {}\mRightarrow{}  b  \mequiv{}  c)


By

---

Latex:
Auto

---

Home Index