---

Step * of Lemma cong-tri-implies-cong-angle2

∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.  (a ≠ b ⇒ b ≠ c ⇒ ab ≅ xy ⇒ bc ≅ yz ⇒ ca ≅ zx ⇒ abc ≅a xyz)
BY
{ (Auto THEN BLemma `cong-tri-implies-cong-angle` THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  ab  \mcong{}  xy  {}\mRightarrow{}  bc  \mcong{}  yz  {}\mRightarrow{}  ca  \mcong{}  zx  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz)


By

---

Latex:
(Auto  THEN  BLemma  `cong-tri-implies-cong-angle`  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index