---

Step * 1 of Lemma geo-krippen-lemma


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| ∨ |ca2| ≤ |ca1|
⊢ m1_c_m2
BY
{ D -1 }

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|
⊢ m1_c_m2

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. |ca2| ≤ |ca1|
⊢ m1_c_m2

---

Latex:

---

Latex:

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|  \mvee{}  |ca2|  \mleq{}  |ca1|
\mvdash{}  m1\_c\_m2


By

---

Latex:
D  -1

---

Home Index