---

Step * of Lemma geo-triangles-between

∀e:HeytingGeometry. ∀a,b,c,p,q:Point.  (a # bc ⇒ b-p-a ⇒ b-q-c ⇒ p # bq)
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. a # bc
8. b-p-a
9. b-q-c
⊢ p # bq

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,p,q:Point.    (a  \#  bc  {}\mRightarrow{}  b-p-a  {}\mRightarrow{}  b-q-c  {}\mRightarrow{}  p  \#  bq)


By

---

Latex:
Auto

---

Home Index