---

Step * of Lemma geo-seg-congruent_functionality

∀e:BasicGeometry. ∀s1,s2,t1,t2:geo-segment(e).
  (geo-seg-congruent(e; s1; t1)
  ⇒ geo-seg-congruent(e; s2; t2)
  ⇒ (geo-seg-congruent(e; s1; s2) ⇐⇒ geo-seg-congruent(e; t1; t2)))
BY
{ Auto }

1
1. e : BasicGeometry
2. s1 : geo-segment(e)
3. s2 : geo-segment(e)
4. t1 : geo-segment(e)
5. t2 : geo-segment(e)
6. geo-seg-congruent(e; s1; t1)
7. geo-seg-congruent(e; s2; t2)
8. geo-seg-congruent(e; s1; s2)
⊢ geo-seg-congruent(e; t1; t2)

2
1. e : BasicGeometry
2. s1 : geo-segment(e)
3. s2 : geo-segment(e)
4. t1 : geo-segment(e)
5. t2 : geo-segment(e)
6. geo-seg-congruent(e; s1; t1)
7. geo-seg-congruent(e; s2; t2)
8. geo-seg-congruent(e; t1; t2)
⊢ geo-seg-congruent(e; s1; s2)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}s1,s2,t1,t2:geo-segment(e).
    (geo-seg-congruent(e;  s1;  t1)
    {}\mRightarrow{}  geo-seg-congruent(e;  s2;  t2)
    {}\mRightarrow{}  (geo-seg-congruent(e;  s1;  s2)  \mLeftarrow{}{}\mRightarrow{}  geo-seg-congruent(e;  t1;  t2)))


By

---

Latex:
Auto

---

Home Index