---

Step * 1 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)
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
BY
{ (FLemma `geo-triangle-implies` [-7] 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
33. b # yx
34. b # xy
35. x ≠ b
36. ¬x_y_b
37. ∀z:Point. (z ≠ y ⇒ Colinear(x;y;z) ⇒ z # yb)
⊢ 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)
24.  y  \#  bx
25.  x  \#  by
26.  x  \#  yb
27.  y  \mneq{}  x
28.  \mneg{}y\_b\_x
29.  \mforall{}z:Point.  (z  \mneq{}  b  {}\mRightarrow{}  Colinear(y;b;z)  {}\mRightarrow{}  z  \#  bx)
30.  x  \#  by
31.  m  :  Point
32.  x-m-y
\mvdash{}  m  \mneq{}  b


By

---

Latex:
(FLemma  `geo-triangle-implies`  [-7]  THEN  Auto)

---

Home Index