---

Step * of Lemma colinear-implies-congruent_or_midpoint

∀e:BasicGeometry. ∀M,A,B:Point.  (Colinear(A;M;B) ⇒ MA ≅ MB ⇒ (¬¬(A ≡ B ∨ A=M=B)))
BY
{ Auto }

1
1. e : BasicGeometry
2. M : Point
3. A : Point
4. B : Point
5. Colinear(A;M;B)
6. MA ≅ MB
⊢ ¬¬(A ≡ B ∨ A=M=B)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}M,A,B:Point.    (Colinear(A;M;B)  {}\mRightarrow{}  MA  \mcong{}  MB  {}\mRightarrow{}  (\mneg{}\mneg{}(A  \mequiv{}  B  \mvee{}  A=M=B)))


By

---

Latex:
Auto

---

Home Index