---

Step * of Lemma geo-seg-congruent-equiv

∀e:BasicGeometry. EquivRel(geo-segment(e);s,t.geo-seg-congruent(e; s; t))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto)) THEN EAuto 1) }

1
1. e : BasicGeometry
2. a : geo-segment(e)
⊢ geo-seg-congruent(e; a; a)

2
1. e : BasicGeometry
2. Sym(geo-segment(e);s,t.geo-seg-congruent(e; s; t))
3. a : geo-segment(e)
4. b : geo-segment(e)
5. c : geo-segment(e)
6. geo-seg-congruent(e; a; b)
7. geo-seg-congruent(e; b; c)
⊢ geo-seg-congruent(e; a; c)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  EquivRel(geo-segment(e);s,t.geo-seg-congruent(e;  s;  t))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto))  THEN  EAuto  1)

---

Home Index