---

Step * of Lemma geo-zero-angle-congruence-out

∀g:EuclideanPlane. ∀a,b,c,x,y:Point.  (abc ≅a xyx ⇒ out(b ac))
BY
{ ((Auto THEN Unfold `geo-cong-angle` 7)
   THEN ExRepD
   THEN ((InstLemma `geo-congruent-preserves-out` [⌜g⌝;⌜y⌝;⌜x'⌝;⌜z'⌝;⌜b⌝;⌜a'⌝;⌜c'⌝]⋅ THEN Auto)
         THENA (InstLemma `geo-between-implies-out2` [⌜g⌝;⌜y⌝;⌜x'⌝;⌜z'⌝;⌜x⌝]⋅ THEN Auto)
         )
   THEN (InstLemma `geo-between-out-implies-out2` [⌜g⌝;⌜b⌝;⌜a⌝;⌜a'⌝;⌜c'⌝]⋅ THEN Auto)
   THEN InstLemma `geo-between-out-implies-out2` [⌜g⌝;⌜b⌝;⌜c⌝;⌜c'⌝;⌜a⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.    (abc  \mcong{}\msuba{}  xyx  {}\mRightarrow{}  out(b  ac))


By

---

Latex:
((Auto  THEN  Unfold  `geo-cong-angle`  7)
  THEN  ExRepD
  THEN  ((InstLemma  `geo-congruent-preserves-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THEN  Auto)
              THENA  (InstLemma  `geo-between-implies-out2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  (InstLemma  `geo-between-out-implies-out2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-between-out-implies-out2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index