---

Step * 1 1 of Lemma geo-triangle-separation


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
7. c # ab
8. a ≠ c
9. ¬a_b_c
10. ∀z:Point. (z ≠ b ⇒ Colinear(a;b;z) ⇒ z # bc)
11. x : Point
12. y : Point
13. Colinear(a;b;x)
14. Colinear(c;b;y)
15. x ≠ b
16. y ≠ b
17. x # bc
18. c # bx
19. x # bc
20. x # cb
21. c ≠ x
22. ¬c_b_x
23. ∀z:Point. (z ≠ b ⇒ Colinear(c;b;z) ⇒ z # bx)
⊢ x # by ∧ (∀m:Point. (x-m-y ⇒ m ≠ b))
BY
{ ((Assert y # bx BY Auto) THEN FLemma `geo-triangle-implies` [-1] THEN Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
7. c # ab
8. a ≠ c
9. ¬a_b_c
10. ∀z:Point. (z ≠ b ⇒ Colinear(a;b;z) ⇒ z # bc)
11. x : Point
12. y : Point
13. Colinear(a;b;x)
14. Colinear(c;b;y)
15. x ≠ b
16. y ≠ b
17. x # bc
18. c # bx
19. x # bc
20. x # cb
21. c ≠ x
22. ¬c_b_x
23. ∀z:Point. (z ≠ b ⇒ Colinear(c;b;z) ⇒ z # bx)
24. y # bx
25. x # by
26. x # yb
27. y ≠ x
28. ¬y_b_x
29. ∀z:Point. (z ≠ b ⇒ Colinear(y;b;z) ⇒ z # bx)
30. x # by
31. m : Point
32. x-m-y
⊢ m ≠ b

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  c  \#  ba
7.  c  \#  ab
8.  a  \mneq{}  c
9.  \mneg{}a\_b\_c
10.  \mforall{}z:Point.  (z  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;z)  {}\mRightarrow{}  z  \#  bc)
11.  x  :  Point
12.  y  :  Point
13.  Colinear(a;b;x)
14.  Colinear(c;b;y)
15.  x  \mneq{}  b
16.  y  \mneq{}  b
17.  x  \#  bc
18.  c  \#  bx
19.  x  \#  bc
20.  x  \#  cb
21.  c  \mneq{}  x
22.  \mneg{}c\_b\_x
23.  \mforall{}z:Point.  (z  \mneq{}  b  {}\mRightarrow{}  Colinear(c;b;z)  {}\mRightarrow{}  z  \#  bx)
\mvdash{}  x  \#  by  \mwedge{}  (\mforall{}m:Point.  (x-m-y  {}\mRightarrow{}  m  \mneq{}  b))


By

---

Latex:
((Assert  y  \#  bx  BY  Auto)  THEN  FLemma  `geo-triangle-implies`  [-1]  THEN  Auto)

---

Home Index