---

Step * 1 1 2 1 of Lemma segment-intersection


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ab
6. A : Point
7. c-a-A
8. aA ≅ cb
9. B : Point
10. c-b-B
11. bB ≅ ca
12. x : Point
13. B-x-a
14. A-x-b
15. x@0 : Point
16. a-x@0-b
17. c-x@0-x
⊢ ∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)
BY
{ ((InstConcl [⌜x@0⌝;⌜x⌝]⋅ THENA Auto) THEN GenRepD) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ab
6. A : Point
7. c-a-A
8. aA ≅ cb
9. B : Point
10. c-b-B
11. bB ≅ ca
12. x : Point
13. B-x-a
14. A-x-b
15. x@0 : Point
16. a-x@0-b
17. c-x@0-x
⊢ Colinear(a;b;x@0)

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  c  \#  ab
6.  A  :  Point
7.  c-a-A
8.  aA  \00D0  cb
9.  B  :  Point
10.  c-b-B
11.  bB  \00D0  ca
12.  x  :  Point
13.  B-x-a
14.  A-x-b
15.  x@0  :  Point
16.  a-x@0-b
17.  c-x@0-x
\mvdash{}  \mexists{}p,q:Point.  (Colinear(a;b;p)  \mwedge{}  c-p-q)


By

---

Latex:
((InstConcl  [\mkleeneopen{}x@0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  GenRepD)

---

Home Index