---

Step * of Lemma geo-triangle-colinear3

∀e:HeytingGeometry. ∀a,b,c,x,y,z:Point.
  (a # bc ⇒ x ≠ b ⇒ Colinear(a;b;x) ⇒ y ≠ c ⇒ Colinear(b;c;y) ⇒ z ≠ x ⇒ Colinear(c;x;z) ⇒ x # yz)
BY
{ (Auto THEN (FLemma `geo-triangle-colinear2` [-5;-3] THENA Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x ≠ b
10. Colinear(a;b;x)
11. y ≠ c
12. Colinear(b;c;y)
13. z ≠ x
14. Colinear(c;x;z)
15. x # yc
⊢ x # yz

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (a  \#  bc
    {}\mRightarrow{}  x  \mneq{}  b
    {}\mRightarrow{}  Colinear(a;b;x)
    {}\mRightarrow{}  y  \mneq{}  c
    {}\mRightarrow{}  Colinear(b;c;y)
    {}\mRightarrow{}  z  \mneq{}  x
    {}\mRightarrow{}  Colinear(c;x;z)
    {}\mRightarrow{}  x  \#  yz)


By

---

Latex:
(Auto  THEN  (FLemma  `geo-triangle-colinear2`  [-5;-3]  THENA  Auto))

---

Home Index