---

Step * 1 1 1 of Lemma segment-intersection

.....wf..... 
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
⊢ c ∈ {c:Point| c # AB} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
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
⊢ c # AB

---

Latex:

---

Latex:
.....wf..... 
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{}  c  \mmember{}  \{c:Point|  c  \#  AB\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index