---

Step * of Lemma perp-aux2

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index