---

Step * of Lemma geo-colinear-congruence2

∀e:BasicGeometry. ∀A,B,C,C':Point.  (A ≠ B ⇒ Colinear(A;B;C) ⇒ 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 ≠ B
7. Colinear(A;B;C)
8. AC ≅ AC'
9. BC ≅ BC'
⊢ C ≡ C'

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index