---

Step * 1 1 of Lemma symmetry_preserves_midpoint


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e1 : Point
7. f : Point
8. z : Point
9. a=z=d
10. b=z=e1
11. c=z=f
12. a=b=c
13. d_e1_f
⊢ d=e1=f
BY
{ (Unfold `geo-midpoint` 0 THEN D 0) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e1 : Point
7. f : Point
8. z : Point
9. a=z=d
10. b=z=e1
11. c=z=f
12. a=b=c
13. d_e1_f
⊢ d_e1_f

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e1 : Point
7. f : Point
8. z : Point
9. a=z=d
10. b=z=e1
11. c=z=f
12. a=b=c
13. d_e1_f
⊢ de1 ≅ e1f

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e1  :  Point
7.  f  :  Point
8.  z  :  Point
9.  a=z=d
10.  b=z=e1
11.  c=z=f
12.  a=b=c
13.  d\_e1\_f
\mvdash{}  d=e1=f


By

---

Latex:
(Unfold  `geo-midpoint`  0  THEN  D  0)

---

Home Index