---

Step * 1 1 of Lemma isosceles-mid-exists


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
7. a # b
8. b # c
9. c # a
10. ¬a-b-c
11. ¬b-c-a
12. ¬c-a-b
13. ∀x,y:Point.  (((Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x # b ∧ y # b) ⇒ (x # by ∧ (∀m:Point. (x-m-y ⇒ m # b))))
14. p : Point
15. b-a-p
16. ap ≅ ba
17. q : Point
18. b-c-q
19. cq ≅ ba
⊢ b ∈ {c:Point| c # pq} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
7. a # b
8. b # c
9. c # a
10. ¬a-b-c
11. ¬b-c-a
12. ¬c-a-b
13. ∀x,y:Point.  (((Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x # b ∧ y # b) ⇒ (x # by ∧ (∀m:Point. (x-m-y ⇒ m # b))))
14. p : Point
15. b-a-p
16. ap ≅ ba
17. q : Point
18. b-c-q
19. cq ≅ ba
⊢ b # pq

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  ab  \mcong{}  cb
7.  a  \#  b
8.  b  \#  c
9.  c  \#  a
10.  \mneg{}a-b-c
11.  \mneg{}b-c-a
12.  \mneg{}c-a-b
13.  \mforall{}x,y:Point.
            (((Colinear(a;b;x)  \mwedge{}  Colinear(c;b;y))  \mwedge{}  x  \#  b  \mwedge{}  y  \#  b)
            {}\mRightarrow{}  (x  \#  by  \mwedge{}  (\mforall{}m:Point.  (x-m-y  {}\mRightarrow{}  m  \#  b))))
14.  p  :  Point
15.  b-a-p
16.  ap  \mcong{}  ba
17.  q  :  Point
18.  b-c-q
19.  cq  \mcong{}  ba
\mvdash{}  b  \mmember{}  \{c:Point|  c  \#  pq\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index