---

Step * of Lemma angle-cong-preserves-straight-angle

∀g:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (x_y_z ⇒ abc ≅a xyz ⇒ a-b-c)
BY
{ ((((Auto THEN D 0 THEN Auto) THEN Unfold `geo-cong-angle` -1) THEN ExRepD)
   THEN (InstLemma `geo-congruent-preserves-strict-between` [⌜g⌝;⌜z'⌝;⌜y⌝;⌜x'⌝;⌜c'⌝;⌜b⌝;⌜a'⌝]⋅ THEN Auto)
   THEN D 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (x\_y\_z  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  a-b-c)


By

---

Latex:
((((Auto  THEN  D  0  THEN  Auto)  THEN  Unfold  `geo-cong-angle`  -1)  THEN  ExRepD)
  THEN  (InstLemma  `geo-congruent-preserves-strict-between`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}
              THEN  Auto
              )
  THEN  D  0
  THEN  EAuto  1)

---

Home Index