---

Step * of Lemma straight-angles-congruent

∀g:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (a-b-c ⇒ x-y-z ⇒ abc ≅a xyz)
BY
{ (((Auto THEN Unfold `geo-cong-angle` 0) THEN GenRepD THEN Auto)
   THEN ((gProperProlong  ⌜b⌝⌜a⌝`A'⌜y⌝⌜x⌝⋅ THENA Auto)
         THEN (gProperProlong  ⌜b⌝⌜c⌝`C'⌜y⌝⌜z⌝⋅ THENA Auto)
         THEN (gProperProlong  ⌜y⌝⌜x⌝`X'⌜a⌝⌜b⌝⋅ THENA Auto)
         THEN (gProperProlong  ⌜y⌝⌜z⌝`Z'⌜b⌝⌜c⌝⋅ THENA Auto)
         THEN InstConcl [⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅
         THEN Auto)
   THEN ((Assert A_b_C BY
                Auto)
         THEN (Assert X_y_Z BY
                     Auto)
         THEN (FLemma `geo-add-length-between` [-1] THENA Auto)
         THEN (FLemma `geo-add-length-between` [-3] THENA Auto))
   THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(((Auto  THEN  Unfold  `geo-cong-angle`  0)  THEN  GenRepD  THEN  Auto)
  THEN  ((gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}`X'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}`Z'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
              THEN  Auto)
  THEN  ((Assert  A\_b\_C  BY
                            Auto)
              THEN  (Assert  X\_y\_Z  BY
                                      Auto)
              THEN  (FLemma  `geo-add-length-between`  [-1]  THENA  Auto)
              THEN  (FLemma  `geo-add-length-between`  [-3]  THENA  Auto))
  THEN  EAuto  1)

---

Home Index