---

Step * 1 1 of Lemma geo-krippen-aux

.....assertion..... 
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c : Point
7. m1 : Point
8. m2 : Point
9. a1_c_a2
10. b1_c_b2
11. ca1 ≅ cb1
12. ca2 ≅ cb2
13. a1=m1=b1
14. a2=m2=b2
15. |ca1| ≤ |ca2|
16. a2 ≠ c
17. a : Point
18. a2=c=a
19. b : Point
20. b2=c=b
21. m2 ≠ c
22. m : Point
23. m2=c=m
⊢ a=m=b
BY
{ (Unfold `geo-midpoint` 0 THEN D 0) }

1
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c : Point
7. m1 : Point
8. m2 : Point
9. a1_c_a2
10. b1_c_b2
11. ca1 ≅ cb1
12. ca2 ≅ cb2
13. a1=m1=b1
14. a2=m2=b2
15. |ca1| ≤ |ca2|
16. a2 ≠ c
17. a : Point
18. a2=c=a
19. b : Point
20. b2=c=b
21. m2 ≠ c
22. m : Point
23. m2=c=m
⊢ a_m_b

2
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c : Point
7. m1 : Point
8. m2 : Point
9. a1_c_a2
10. b1_c_b2
11. ca1 ≅ cb1
12. ca2 ≅ cb2
13. a1=m1=b1
14. a2=m2=b2
15. |ca1| ≤ |ca2|
16. a2 ≠ c
17. a : Point
18. a2=c=a
19. b : Point
20. b2=c=b
21. m2 ≠ c
22. m : Point
23. m2=c=m
⊢ am ≅ mb

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c  :  Point
7.  m1  :  Point
8.  m2  :  Point
9.  a1\_c\_a2
10.  b1\_c\_b2
11.  ca1  \00D0  cb1
12.  ca2  \00D0  cb2
13.  a1=m1=b1
14.  a2=m2=b2
15.  |ca1|  \mleq{}  |ca2|
16.  a2  \mneq{}  c
17.  a  :  Point
18.  a2=c=a
19.  b  :  Point
20.  b2=c=b
21.  m2  \mneq{}  c
22.  m  :  Point
23.  m2=c=m
\mvdash{}  a=m=b


By

---

Latex:
(Unfold  `geo-midpoint`  0  THEN  D  0)

---

Home Index