---

Step * of Lemma geo-out-triangle

∀e:HeytingGeometry. ∀a,b,c,a',c':Point.  (b # ac ⇒ (out(b aa') ∧ out(b cc')) ⇒ b # a'c')
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. b # ac
8. out(b aa')
9. out(b cc')
⊢ b # a'c'

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,a',c':Point.    (b  \#  ac  {}\mRightarrow{}  (out(b  aa')  \mwedge{}  out(b  cc'))  {}\mRightarrow{}  b  \#  a'c')


By

---

Latex:
Auto

---

Home Index