---

Step * of Lemma geo-out-preserves-lt-angle

∀e:EuclideanPlane. ∀a,b,c,a',c',x,y,z:Point.  (a # bc ⇒ out(b aa') ⇒ out(b cc') ⇒ abc < xyz ⇒ a'bc' < xyz)
BY
{ (Auto
   THEN (Assert abc ≅a a'bc' BY
               (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a'⌝;⌜c'⌝;⌜a⌝;⌜c⌝]⋅ THEN EAuto 1))
   THEN InstLemma `geo-cong-angle-preserves-lt-angle` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a'⌝;⌜b⌝;⌜c'⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',c',x,y,z:Point.
    (a  \#  bc  {}\mRightarrow{}  out(b  aa')  {}\mRightarrow{}  out(b  cc')  {}\mRightarrow{}  abc  <  xyz  {}\mRightarrow{}  a'bc'  <  xyz)


By

---

Latex:
(Auto
  THEN  (Assert  abc  \mcong{}\msuba{}  a'bc'  BY
                          (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{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]
                            \mcdot{}
                            THEN  EAuto  1
                            ))
  THEN  InstLemma  `geo-cong-angle-preserves-lt-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index