---

Step * of Lemma geo-strict-between-congruence

∀e:BasicGeometry. ∀A,B,C,C':Point.  (A_C_B ⇒ AC ≅ AC' ⇒ BC ≅ BC' ⇒ C ≡ C')
BY
{ Auto }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. C' : Point
6. A_C_B
7. AC ≅ AC'
8. BC ≅ BC'
⊢ C ≡ C'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,C':Point.    (A\_C\_B  {}\mRightarrow{}  AC  \00D0  AC'  {}\mRightarrow{}  BC  \00D0  BC'  {}\mRightarrow{}  C  \mequiv{}  C')


By

---

Latex:
Auto

---

Home Index