---

Step * 1 2 1 1 1 1 1 2 1 of Lemma isosceles-mid-exists

.....assertion..... 
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
7. a # b
8. b # c
9. c # a
10. ¬a-b-c
11. ¬b-c-a
12. ¬c-a-b
13. ∀x,y:Point.  (((Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x # b ∧ y # b) ⇒ (x # by ∧ (∀m:Point. (x-m-y ⇒ m # b))))
14. p : Point
15. b-a-p
16. ap ≅ ba
17. q : Point
18. b-c-q
19. cq ≅ ba
20. x : Point
21. q-x-a
22. p-x-c
23. p # bc
24. ∀m:Point. (p-m-c ⇒ m # b)
25. p # b
26. b # c
27. c # p
28. ¬p-b-c
29. ¬b-c-p
30. ¬c-p-b
31. a # bq
32. ∀m:Point. (a-m-q ⇒ m # b)
33. a # b
34. b # q
35. q # a
36. ¬a-b-q
37. ¬b-q-a
38. ¬q-a-b
39. p # c
40. x # b
41. p-x-c
42. q-x-a
43. y : Point
44. B(byx)
45. B(cya)
46. B(ayc)
47. y # b
48. x # b
49. qa ≅ pc
50. b' : Point
51. B(pb'c)
52. qx ≅ pb'
53. xa ≅ b'c
54. pc ≅ qa
⊢ b' ≡ x
BY
{ (InstLemma `geo-intersection-unicity` [⌜e⌝;⌜p⌝;⌜c⌝;⌜q⌝;⌜a⌝]⋅ THENA Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
7. a # b
8. b # c
9. c # a
10. ¬a-b-c
11. ¬b-c-a
12. ¬c-a-b
13. ∀x,y:Point.  (((Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x # b ∧ y # b) ⇒ (x # by ∧ (∀m:Point. (x-m-y ⇒ m # b))))
14. p : Point
15. b-a-p
16. ap ≅ ba
17. q : Point
18. b-c-q
19. cq ≅ ba
20. x : Point
21. q-x-a
22. p-x-c
23. p # bc
24. ∀m:Point. (p-m-c ⇒ m # b)
25. p # b
26. b # c
27. c # p
28. ¬p-b-c
29. ¬b-c-p
30. ¬c-p-b
31. a # bq
32. ∀m:Point. (a-m-q ⇒ m # b)
33. a # b
34. b # q
35. q # a
36. ¬a-b-q
37. ¬b-q-a
38. ¬q-a-b
39. p # c
40. x # b
41. p-x-c
42. q-x-a
43. y : Point
44. B(byx)
45. B(cya)
46. B(ayc)
47. y # b
48. x # b
49. qa ≅ pc
50. b' : Point
51. B(pb'c)
52. qx ≅ pb'
53. xa ≅ b'c
54. pc ≅ qa
55. ∀p@0,q@0:Point.
      ((¬Colinear(p;c;q))
      ⇒ q # a
      ⇒ Colinear(p;c;p@0)
      ⇒ Colinear(p;c;q@0)
      ⇒ Colinear(q;a;p@0)
      ⇒ Colinear(q;a;q@0)
      ⇒ p@0 ≡ q@0)
⊢ b' ≡ x

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  ab  \mcong{}  cb
7.  a  \#  b
8.  b  \#  c
9.  c  \#  a
10.  \mneg{}a-b-c
11.  \mneg{}b-c-a
12.  \mneg{}c-a-b
13.  \mforall{}x,y:Point.
            (((Colinear(a;b;x)  \mwedge{}  Colinear(c;b;y))  \mwedge{}  x  \#  b  \mwedge{}  y  \#  b)
            {}\mRightarrow{}  (x  \#  by  \mwedge{}  (\mforall{}m:Point.  (x-m-y  {}\mRightarrow{}  m  \#  b))))
14.  p  :  Point
15.  b-a-p
16.  ap  \mcong{}  ba
17.  q  :  Point
18.  b-c-q
19.  cq  \mcong{}  ba
20.  x  :  Point
21.  q-x-a
22.  p-x-c
23.  p  \#  bc
24.  \mforall{}m:Point.  (p-m-c  {}\mRightarrow{}  m  \#  b)
25.  p  \#  b
26.  b  \#  c
27.  c  \#  p
28.  \mneg{}p-b-c
29.  \mneg{}b-c-p
30.  \mneg{}c-p-b
31.  a  \#  bq
32.  \mforall{}m:Point.  (a-m-q  {}\mRightarrow{}  m  \#  b)
33.  a  \#  b
34.  b  \#  q
35.  q  \#  a
36.  \mneg{}a-b-q
37.  \mneg{}b-q-a
38.  \mneg{}q-a-b
39.  p  \#  c
40.  x  \#  b
41.  p-x-c
42.  q-x-a
43.  y  :  Point
44.  B(byx)
45.  B(cya)
46.  B(ayc)
47.  y  \#  b
48.  x  \#  b
49.  qa  \mcong{}  pc
50.  b'  :  Point
51.  B(pb'c)
52.  qx  \mcong{}  pb'
53.  xa  \mcong{}  b'c
54.  pc  \mcong{}  qa
\mvdash{}  b'  \mequiv{}  x


By

---

Latex:
(InstLemma  `geo-intersection-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index