---

Step * 1 2 of Lemma geo-krippen-aux


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
24. a=m=b
⊢ m1_c_m2
BY
{ (Assert |ca1| ≤ |ca| BY
         OnMaybeHyp 18 (\h. (D h THEN Complete (Auto)))) }

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
24. a=m=b
25. |ca1| ≤ |ca|
⊢ 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|
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
24.  a=m=b
\mvdash{}  m1\_c\_m2


By

---

Latex:
(Assert  |ca1|  \mleq{}  |ca|  BY
              OnMaybeHyp  18  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))

---

Home Index