---

Step * of Lemma eu-congruent-iff-length

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  uiff(ab=cd;|ab| = |cd| ∈ {p:Point| O_X_p} )
BY
{ ((Auto THEN Try ((FLemma `eu-seg-congruent-iff-length` [-1] THEN Auto)))
   THEN BLemma `eu-seg-congruent-iff-length`
   THEN Auto
   THEN RepUR ``eu-seg-congruent`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Try  ((FLemma  `eu-seg-congruent-iff-length`  [-1]  THEN  Auto)))
  THEN  BLemma  `eu-seg-congruent-iff-length`
  THEN  Auto
  THEN  RepUR  ``eu-seg-congruent``  0
  THEN  Auto)

---

Home Index