---

Step * 1 of Lemma geo-zero-angle-congruence-subst


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc ≅a xyx
9. out(b ac)
⊢ aba ≅a xyx
BY
{ (InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜x⌝;⌜a⌝;⌜a⌝;⌜x⌝;⌜x⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  abc  \mcong{}\msuba{}  xyx
9.  out(b  ac)
\mvdash{}  aba  \mcong{}\msuba{}  xyx


By

---

Latex:
(InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index