---

Step * 1 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
⊢ am ≅ mb
BY
{ ((D 14 THEN InstLemma `geo-midpoint-diagonals-congruent2` [⌜e⌝;⌜a2⌝;⌜m2⌝;⌜m2⌝;⌜b2⌝;⌜a⌝;⌜m⌝;⌜m⌝;⌜b⌝;⌜c⌝]⋅) THEN Auto) }

---

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
\mvdash{}  am  \00D0  mb


By

---

Latex:
((D  14
    THEN  InstLemma  `geo-midpoint-diagonals-congruent2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}m2\mkleeneclose{};\mkleeneopen{}m2\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
    )
  THEN  Auto
  )

---

Home Index