---

Step * of Lemma out-cong-angle

∀e:BasicGeometry. ∀a,b,c,a',c':Point.  (out(b cc') ⇒ out(b aa') ⇒ abc ≅a a'bc')
BY
{ (Auto
   THEN (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',c':Point.    (out(b  cc')  {}\mRightarrow{}  out(b  aa')  {}\mRightarrow{}  abc  \00D0\msuba{}  a'bc')


By

---

Latex:
(Auto
  THEN  (InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto
  THEN  EAuto  1)

---

Home Index