---

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


1. e : BasicGeometry
2. ∀[s,t:geo-segment(e)].  uiff(geo-seg1(s)geo-seg2(s) ≅ geo-seg1(t)geo-seg2(t);|s| ≡ |t|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. ab ≅ cd
8. uiff(ab ≅ cd;|ab| ≡ |cd|)
9. |ab| ≡ |cd|
⊢ |ab| = |cd| ∈ Length
BY
{ (EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  \mforall{}[s,t:geo-segment(e)].    uiff(geo-seg1(s)geo-seg2(s)  \00D0  geo-seg1(t)geo-seg2(t);|s|  \mequiv{}  |t|)
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  ab  \00D0  cd
8.  uiff(ab  \00D0  cd;|ab|  \mequiv{}  |cd|)
9.  |ab|  \mequiv{}  |cd|
\mvdash{}  |ab|  =  |cd|


By

---

Latex:
(EqTypeCD  THEN  Auto)

---

Home Index