---

Step * of Lemma vert-angles-congruent

∀e:HeytingGeometry. ∀b,a,a',c,c':Point.  (a-b-a' ⇒ c-b-c' ⇒ a # bc ⇒ abc ≅a a'bc')
BY
{ Auto }

1
1. e : HeytingGeometry
2. b : Point
3. a : Point
4. a' : Point
5. c : Point
6. c' : Point
7. a-b-a'
8. c-b-c'
9. a # bc
⊢ abc ≅a a'bc'

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}b,a,a',c,c':Point.    (a-b-a'  {}\mRightarrow{}  c-b-c'  {}\mRightarrow{}  a  \#  bc  {}\mRightarrow{}  abc  \mcong{}\msuba{}  a'bc')


By

---

Latex:
Auto

---

Home Index