---

Step * of Lemma p6-aux-bet-preserves-angle

∀e:HeytingGeometry. ∀a,b,c,d:Point.  (a # bc ⇒ (a_d_b ∧ a ≠ d) ⇒ cab ≅a cad)
BY
{ (Auto
   THEN Unfold `geo-cong-angle` 0
   THEN (gProlong ⌜a⌝⌜d⌝`b\''⌜d⌝⌜b⌝⋅ THEN Auto)
   THEN InstConcl [⌜c⌝;⌜b⌝;⌜c⌝;⌜b⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,d:Point.    (a  \#  bc  {}\mRightarrow{}  (a\_d\_b  \mwedge{}  a  \mneq{}  d)  {}\mRightarrow{}  cab  \mcong{}\msuba{}  cad)


By

---

Latex:
(Auto
  THEN  Unfold  `geo-cong-angle`  0
  THEN  (gProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`b\mbackslash{}''\mkleeneopen{}d\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  InstConcl  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index