---

Step * of Lemma geo-cong-angle-symmetry

No Annotations
∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
  (xyz ≅a abc ⇒ {zyx ≅a abc ∧ xyz ≅a cba ∧ zyx ≅a cba ∧ abc ≅a xyz ∧ cba ≅a xyz ∧ abc ≅a zyx ∧ cba ≅a zyx})
BY
{ (Intros
   THEN (Assert a # b ∧ c # b ∧ x # y ∧ z # y BY
               (D -1 THEN Auto))
   THEN PromoteHyp (-1) (-2)
   THEN ExRepD
   THEN EAuto 1) }

1
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (xyz  \mcong{}\msuba{}  abc
    {}\mRightarrow{}  \{zyx  \mcong{}\msuba{}  abc  \mwedge{}  xyz  \mcong{}\msuba{}  cba  \mwedge{}  zyx  \mcong{}\msuba{}  cba  \mwedge{}  abc  \mcong{}\msuba{}  xyz  \mwedge{}  cba  \mcong{}\msuba{}  xyz  \mwedge{}  abc  \mcong{}\msuba{}  zyx  \mwedge{}  cba  \mcong{}\msuba{}  zyx\})


By

---

Latex:
(Intros
  THEN  (Assert  a  \#  b  \mwedge{}  c  \#  b  \mwedge{}  x  \#  y  \mwedge{}  z  \#  y  BY
                          (D  -1  THEN  Auto))
  THEN  PromoteHyp  (-1)  (-2)
  THEN  ExRepD
  THEN  EAuto  1)

---

Home Index