---

Step * of Lemma cong3-implies-conga

∀e:BasicGeometry. ∀a,b,c,d,E,f:Point.  (a ≠ b ⇒ b ≠ c ⇒ Cong3(abc,dEf) ⇒ abc ≅a dEf)
BY
{ ((Auto THEN D -1) THEN (D 0 THENL [Auto; (InstConcl [⌜a⌝;⌜c⌝;⌜d⌝;⌜f⌝]⋅ THEN Auto)])) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,E,f:Point.    (a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  Cong3(abc,dEf)  {}\mRightarrow{}  abc  \mcong{}\msuba{}  dEf)


By

---

Latex:
((Auto  THEN  D  -1)  THEN  (D  0  THENL  [Auto;  (InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)]))

---

Home Index