---

Step * of Lemma geo-krippen-lemma

∀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 ⇒ m1_c_m2)
BY
{ (Auto
   THEN (InstLemma  `geo-le-cases` [⌜e⌝;⌜|ca1|⌝;⌜|ca2|⌝]⋅ THENA Auto)
   THEN ((DoubleNegation THENM SupposeMore (-1)) THENA Auto)
   THEN (RemoveDoubleNegation THENA 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| ∨ |ca2| ≤ |ca1|
⊢ 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{}  m1\_c\_m2)


By

---

Latex:
(Auto
  THEN  (InstLemma    `geo-le-cases`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}|ca1|\mkleeneclose{};\mkleeneopen{}|ca2|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((DoubleNegation  THENM  SupposeMore  (-1))  THENA  Auto)
  THEN  (RemoveDoubleNegation  THENA  Auto))

---

Home Index