---

Step * of Lemma cong-tri-implies-all-cong-angle

No Annotations
∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
  (Cong3(abc,xyz) ⇒ a # b ⇒ b # c ⇒ c # a ⇒ x # y ⇒ y # z ⇒ z # x ⇒ {abc ≅a xyz ∧ bca ≅a yzx ∧ cab ≅a zxy})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN BLemma `cong-tri-implies-cong-angle`
   THEN Auto
   THEN RepeatFor 2 ((BLemma `geo-cong-tri-symmetry` THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (Cong3(abc,xyz)
    {}\mRightarrow{}  a  \#  b
    {}\mRightarrow{}  b  \#  c
    {}\mRightarrow{}  c  \#  a
    {}\mRightarrow{}  x  \#  y
    {}\mRightarrow{}  y  \#  z
    {}\mRightarrow{}  z  \#  x
    {}\mRightarrow{}  \{abc  \mcong{}\msuba{}  xyz  \mwedge{}  bca  \mcong{}\msuba{}  yzx  \mwedge{}  cab  \mcong{}\msuba{}  zxy\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  BLemma  `cong-tri-implies-cong-angle`
  THEN  Auto
  THEN  RepeatFor  2  ((BLemma  `geo-cong-tri-symmetry`  THEN  Auto)))

---

Home Index