---

Step * of Lemma geo-be-end-eq

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index