---

Step * 1 of Lemma geo-seg-congruent_functionality


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)
BY
{ ((InstLemma `geo-seg-congruent_transitivity` [⌜e⌝;⌜t1⌝;⌜s1⌝;⌜s2⌝]⋅ THEN EAuto 1)
   THEN InstLemma `geo-seg-congruent_transitivity` [⌜e⌝;⌜t1⌝;⌜s2⌝;⌜t2⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

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)
\mvdash{}  geo-seg-congruent(e;  t1;  t2)


By

---

Latex:
((InstLemma  `geo-seg-congruent\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}s2\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  InstLemma  `geo-seg-congruent\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{};\mkleeneopen{}s2\mkleeneclose{};\mkleeneopen{}t2\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index