---

Step * 1 of Lemma colinear-implies-congruent_or_midpoint


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)
BY
{ D 0 }

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

2
.....wf..... 
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:

1.  e  :  BasicGeometry
2.  M  :  Point
3.  A  :  Point
4.  B  :  Point
5.  Colinear(A;M;B)
6.  MA  \mcong{}  MB
\mvdash{}  \mneg{}\mneg{}(A  \mequiv{}  B  \mvee{}  A=M=B)


By

---

Latex:
D  0

---

Home Index