---

Step * 1 1 1 1 1 1 1 1 of Lemma at-most-one-midpoint


1. e : BasicGeometry
2. P : Point
3. P' : Point
4. A : Point
5. B : Point
6. P=A=P'
7. P=B=P'
8. A ≠ B
9. PB ≅ P'B
10. B ≠ A
11. B' : Point
12. B=A=B'
13. P'=A=P
14. PB' ≅ P'B
⊢ A ≡ B
BY
{ Assert ⌜PB ≅ PB'⌝⋅ }

1
.....assertion..... 
1. e : BasicGeometry
2. P : Point
3. P' : Point
4. A : Point
5. B : Point
6. P=A=P'
7. P=B=P'
8. A ≠ B
9. PB ≅ P'B
10. B ≠ A
11. B' : Point
12. B=A=B'
13. P'=A=P
14. PB' ≅ P'B
⊢ PB ≅ PB'

2
1. e : BasicGeometry
2. P : Point
3. P' : Point
4. A : Point
5. B : Point
6. P=A=P'
7. P=B=P'
8. A ≠ B
9. PB ≅ P'B
10. B ≠ A
11. B' : Point
12. B=A=B'
13. P'=A=P
14. PB' ≅ P'B
15. PB ≅ PB'
⊢ A ≡ B

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  P  :  Point
3.  P'  :  Point
4.  A  :  Point
5.  B  :  Point
6.  P=A=P'
7.  P=B=P'
8.  A  \mneq{}  B
9.  PB  \00D0  P'B
10.  B  \mneq{}  A
11.  B'  :  Point
12.  B=A=B'
13.  P'=A=P
14.  PB'  \00D0  P'B
\mvdash{}  A  \mequiv{}  B


By

---

Latex:
Assert  \mkleeneopen{}PB  \00D0  PB'\mkleeneclose{}\mcdot{}

---

Home Index