---

Step * of Lemma geo-midpoint_functionality

∀e:BasicGeometry. ∀m,a,b,m',a',b':Point.  (m ≡ m' ⇒ a ≡ a' ⇒ b ≡ b' ⇒ {a=m=b ⇒ a'=m'=b'})
BY
{ ((Unfold `geo-midpoint` 0 THEN Unfold `guard` 0) THEN Auto) }

1
1. e : BasicGeometry
2. m : Point
3. a : Point
4. b : Point
5. m' : Point
6. a' : Point
7. b' : Point
8. m ≡ m'
9. a ≡ a'
10. b ≡ b'
11. a_m_b
12. am ≅ mb
⊢ a'_m'_b'

2
1. e : BasicGeometry
2. m : Point
3. a : Point
4. b : Point
5. m' : Point
6. a' : Point
7. b' : Point
8. m ≡ m'
9. a ≡ a'
10. b ≡ b'
11. a_m_b
12. am ≅ mb
13. a'_m'_b'
⊢ a'm' ≅ m'b'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}m,a,b,m',a',b':Point.    (m  \mequiv{}  m'  {}\mRightarrow{}  a  \mequiv{}  a'  {}\mRightarrow{}  b  \mequiv{}  b'  {}\mRightarrow{}  \{a=m=b  {}\mRightarrow{}  a'=m'=b'\})


By

---

Latex:
((Unfold  `geo-midpoint`  0  THEN  Unfold  `guard`  0)  THEN  Auto)

---

Home Index