---

Step * of Lemma geo-krippen-aux

∀e:BasicGeometry. ∀a1,a2,b1,b2,c,m1,m2:Point.
  (a1_c_a2 ⇒ b1_c_b2 ⇒ ca1 ≅ cb1 ⇒ ca2 ≅ cb2 ⇒ a1=m1=b1 ⇒ a2=m2=b2 ⇒ |ca1| ≤ |ca2| ⇒ m1_c_m2)
BY
{ (Auto THEN gSymmetricPoint ⌜c⌝ ⌜a2⌝ `a'⋅ THEN gSymmetricPoint ⌜c⌝ ⌜b2⌝ `b'⋅ THEN gSymmetricPoint ⌜c⌝ ⌜m2⌝ `m'⋅) }

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

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a1,a2,b1,b2,c,m1,m2:Point.
    (a1\_c\_a2  {}\mRightarrow{}  b1\_c\_b2  {}\mRightarrow{}  ca1  \00D0  cb1  {}\mRightarrow{}  ca2  \00D0  cb2  {}\mRightarrow{}  a1=m1=b1  {}\mRightarrow{}  a2=m2=b2  {}\mRightarrow{}  |ca1|  \mleq{}  |ca2|  {}\mRightarrow{}  m1\_c\_m2)


By

---

Latex:
(Auto
  THEN  gSymmetricPoint  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}a2\mkleeneclose{}  `a'\mcdot{}
  THEN  gSymmetricPoint  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}b2\mkleeneclose{}  `b'\mcdot{}
  THEN  gSymmetricPoint  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}m2\mkleeneclose{}  `m'\mcdot{})

---

Home Index