---

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

---

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


By

---

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

---

Home Index