---

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

∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.  (Cong3(abc,xyz) ⇒ a ≠ b ⇒ b ≠ c ⇒ x ≠ y ⇒ y ≠ z ⇒ abc ≅a xyz)
BY
{ ((Auto THEN Unfold `geo-cong-angle` 0 THEN GenRepD) THEN D 8 THEN InstConcl [⌜a⌝;⌜c⌝;⌜x⌝;⌜z⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (Cong3(abc,xyz)  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  x  \mneq{}  y  {}\mRightarrow{}  y  \mneq{}  z  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz)


By

---

Latex:
((Auto  THEN  Unfold  `geo-cong-angle`  0  THEN  GenRepD)
  THEN  D  8
  THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index