---

Step * of Lemma geo-congruent-iff-length

∀e:BasicGeometry. ∀[a,b,c,d:Point].  uiff(ab ≅ cd;|ab| = |cd| ∈ Length)
BY
{ (InstLemma `geo-seg-congruent-iff-length` []
   THEN ParallelLast'
   THEN Unfold `geo-seg-congruent` 2
   THEN Auto
   THEN (InstHyp [⌜ab⌝;⌜cd⌝] 2⋅ THENA Auto)
   THEN Reduce -1
   THEN (BHyp (-1)  ORELSE FHyp (-1) [-2])) }

1
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

2
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| ∈ Length
8. uiff(ab ≅ cd;|ab| ≡ |cd|)
⊢ |ab| ≡ |cd|

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[a,b,c,d:Point].    uiff(ab  \00D0  cd;|ab|  =  |cd|)


By

---

Latex:
(InstLemma  `geo-seg-congruent-iff-length`  []
  THEN  ParallelLast'
  THEN  Unfold  `geo-seg-congruent`  2
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}ab\mkleeneclose{};\mkleeneopen{}cd\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  (BHyp  (-1)    ORELSE  FHyp  (-1)  [-2]))

---

Home Index