---

Step * 1 of Lemma isosceles-mid-exists


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
⊢ ∃x:Point. a=x=c
BY
{ (((FLemma `geo-triangle-property` [-2] THENA Auto) THEN (FLemma `geo-triangle-separation` [-3] THENA Auto))
   THEN (PropergProlong ⌜b⌝⌜a⌝`p'⌜b⌝⌜a⌝⋅ THENA Auto)
   THEN (PropergProlong ⌜b⌝⌜c⌝`q'⌜b⌝⌜a⌝⋅ THENA Auto)
   THEN (InstLemma `geo-inner-pasch-ex` [⌜e⌝;⌜p⌝;⌜q⌝;⌜b⌝;⌜a⌝;⌜c⌝]⋅ THENA Auto)) }

1
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} 

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

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  ab  \mcong{}  cb
\mvdash{}  \mexists{}x:Point.  a=x=c


By

---

Latex:
(((FLemma  `geo-triangle-property`  [-2]  THENA  Auto)
    THEN  (FLemma  `geo-triangle-separation`  [-3]  THENA  Auto)
    )
  THEN  (PropergProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`p'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (PropergProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`q'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-inner-pasch-ex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index