---

Step * 1 of Lemma geo-midpoint-symmetry


1. e : BasicGeometry
2. m : Point
3. a : Point
4. b : Point
5. B(amb)
6. am ≅ mb
7. B(bma)
⊢ bm ≅ ma
BY
{ ((Assert mb ≅ bm BY
          (Auto THEN BLemma `geo-congruent-left-comm` THEN Auto))
   THEN FLemma `geo-congruent-transitivity` [-3;-1]
   THEN Auto) }

1
1. e : BasicGeometry
2. m : Point
3. a : Point
4. b : Point
5. B(amb)
6. am ≅ mb
7. B(bma)
8. mb ≅ bm
9. am ≅ bm
⊢ bm ≅ ma

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  m  :  Point
3.  a  :  Point
4.  b  :  Point
5.  B(amb)
6.  am  \mcong{}  mb
7.  B(bma)
\mvdash{}  bm  \mcong{}  ma


By

---

Latex:
((Assert  mb  \mcong{}  bm  BY
                (Auto  THEN  BLemma  `geo-congruent-left-comm`  THEN  Auto))
  THEN  FLemma  `geo-congruent-transitivity`  [-3;-1]
  THEN  Auto)

---

Home Index