---

Step * 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
⊢ x ≡ y
BY
{ (InstLemma `geo-intersection-unicity` [⌜e⌝;⌜C⌝;⌜g⌝;⌜B⌝;⌜d⌝;⌜x⌝;⌜y⌝]⋅ THEN Auto) }

1
.....antecedent..... 
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
⊢ ¬Colinear(C;g;B)

---

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
\mvdash{}  x  \mequiv{}  y


By

---

Latex:
(InstLemma  `geo-intersection-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index