---

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

No Annotations
∀e:BasicGeometry. ∀[s,t:geo-segment(e)].  uiff(geo-seg-congruent(e; s; t);|s| ≡ |t|)
BY
{ (Auto THEN Try ((EqTypeCD THEN Auto))) }

1
1. e : BasicGeometry
2. s : geo-segment(e)
3. t : geo-segment(e)
4. geo-seg-congruent(e; s; t)
⊢ |s| ≡ |t|

2
1. e : BasicGeometry
2. s : geo-segment(e)
3. t : geo-segment(e)
4. |s| ≡ |t|
⊢ geo-seg-congruent(e; s; t)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}[s,t:geo-segment(e)].    uiff(geo-seg-congruent(e;  s;  t);|s|  \mequiv{}  |t|)


By

---

Latex:
(Auto  THEN  Try  ((EqTypeCD  THEN  Auto)))

---

Home Index