---

Step * 1 of Lemma geo-cong-angle-symmetry


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # b
9. c # b
10. x # y
11. z # y
12. xyz ≅a abc
⊢ zyx ≅a abc
BY
{ ((Using [`p',⌜c⌝;`q',⌜b⌝;`r',⌜a⌝] (FLemma `geo-cong-angle-transitivity` [-1])⋅ THENA EAuto 1)
   THEN Using [`x',⌜x⌝;`y',⌜y⌝;`z',⌜z⌝] (BLemma `geo-cong-angle-transitivity`)⋅
        THEN EAuto 1
   ) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a  \#  b
9.  c  \#  b
10.  x  \#  y
11.  z  \#  y
12.  xyz  \mcong{}\msuba{}  abc
\mvdash{}  zyx  \mcong{}\msuba{}  abc


By

---

Latex:
((Using  [`p',\mkleeneopen{}c\mkleeneclose{};`q',\mkleeneopen{}b\mkleeneclose{};`r',\mkleeneopen{}a\mkleeneclose{}]  (FLemma  `geo-cong-angle-transitivity`  [-1])\mcdot{}  THENA  EAuto  1)
  THEN  Using  [`x',\mkleeneopen{}x\mkleeneclose{};`y',\mkleeneopen{}y\mkleeneclose{};`z',\mkleeneopen{}z\mkleeneclose{}]  (BLemma  `geo-cong-angle-transitivity`)\mcdot{}
            THEN  EAuto  1
  )

---

Home Index