Step * 1 1 of Lemma segment-intersection


1. HeytingGeometry
2. Point
3. Point
4. Point
5. ab
6. Point
7. c-a-A
8. aA ≅ cb
9. Point
10. c-b-B
11. bB ≅ ca
⊢ ∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)
BY
((InstLemma `geo-inner-pasch-ex` [⌜e⌝;⌜A⌝;⌜B⌝;⌜c⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ExRepD) }

1
.....wf..... 
1. HeytingGeometry
2. Point
3. Point
4. Point
5. ab
6. Point
7. c-a-A
8. aA ≅ cb
9. Point
10. c-b-B
11. bB ≅ ca
⊢ c ∈ {c:Point| AB} 

2
1. HeytingGeometry
2. Point
3. Point
4. Point
5. ab
6. Point
7. c-a-A
8. aA ≅ cb
9. Point
10. c-b-B
11. bB ≅ ca
12. Point
13. B-x-a
14. A-x-b
⊢ ∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)


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
\mvdash{}  \mexists{}p,q:Point.  (Colinear(a;b;p)  \mwedge{}  c-p-q)


By


Latex:
((InstLemma  `geo-inner-pasch-ex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)




Home Index