---

Step * 1 of Lemma geo-seg-congruent-iff-length


1. e : BasicGeometry
2. s : geo-segment(e)
3. t : geo-segment(e)
4. geo-seg-congruent(e; s; t)
⊢ |s| ≡ |t|
BY
{ (Unfold `geo-length` 0 THEN Unfold `geo-seg-congruent` -1 THEN RWO "geo-extend-equal-iff-congruent" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  s  :  geo-segment(e)
3.  t  :  geo-segment(e)
4.  geo-seg-congruent(e;  s;  t)
\mvdash{}  |s|  \mequiv{}  |t|


By

---

Latex:
(Unfold  `geo-length`  0
  THEN  Unfold  `geo-seg-congruent`  -1
  THEN  RWO  "geo-extend-equal-iff-congruent"  0
  THEN  Auto)

---

Home Index