---

Step * 1 1 1 of Lemma geo-double-pasch-same-point


1. e : HeytingGeometry
2. A : Point
3. B : Point
4. C : Point
5. d : Point
6. f : Point
7. g : Point
8. x : Point
9. y : Point
10. A # BC
11. A-d-C
12. A-g-B
13. B-f-C
14. C-x-g
15. C-y-g
16. B-x-d
17. B-y-d
18. A-x-f
19. A-y-f
20. Colinear(C;g;B)
⊢ False
BY
{ (Assert Colinear(A;B;C) BY
         Auto) }

1
1. e : HeytingGeometry
2. A : Point
3. B : Point
4. C : Point
5. d : Point
6. f : Point
7. g : Point
8. x : Point
9. y : Point
10. A # BC
11. A-d-C
12. A-g-B
13. B-f-C
14. C-x-g
15. C-y-g
16. B-x-d
17. B-y-d
18. A-x-f
19. A-y-f
20. Colinear(C;g;B)
21. Colinear(A;B;C)
⊢ False

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  d  :  Point
6.  f  :  Point
7.  g  :  Point
8.  x  :  Point
9.  y  :  Point
10.  A  \#  BC
11.  A-d-C
12.  A-g-B
13.  B-f-C
14.  C-x-g
15.  C-y-g
16.  B-x-d
17.  B-y-d
18.  A-x-f
19.  A-y-f
20.  Colinear(C;g;B)
\mvdash{}  False


By

---

Latex:
(Assert  Colinear(A;B;C)  BY
              Auto)

---

Home Index