---

Step * of Lemma line-circle-continuity

∀e:EuclideanPlane. ∀a,b,p:Point. ∀q:{q:Point| ¬(q = p ∈ Point)} .
  ((∃x:{x:Point| a_x_b ∧ (¬(x = b ∈ Point))} . ∃y:{y:Point| a_b_y} . (ap=ax ∧ aq=ay))
  ⇒ (∃y,z:Point. (ay=ab ∧ az=ab ∧ z_p_q ∧ p_y_q ∧ (¬(y = z ∈ Point)))))
BY
{ (Auto
   THEN ExRepD
   THEN (InstConcl [⌜fst(intersect pq (at radius xy) with Oab )⌝; ⌜snd(intersect pq (at radius xy) with Oab )⌝]⋅
         THENA Auto
         )
   THEN D 1
   THEN (Unhide THENA Auto)
   THEN D 2
   THEN ExRepD) }

1
1. e : EuclideanStructure@i'
2. ∀[a,b:Point].  ab=ba@i'
3. ∀[a,b,p,q,r,s:Point].  (pq=rs) supposing (ab=rs and ab=pq)@i'
4. ∀[a,b,c:Point].  a = b ∈ Point supposing ab=cc@i'
5. ∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)@i'
6. ∀[a,b,c,d,A,B,C,D:Point].
     (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))@i'
7. ∀[a,b:Point].  (¬a-b-a)@i'
8. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
     let x = eu-inner-pasch(e;a;b;c;p;q) in
         p-x-b ∧ q-x-a@i'
9. ∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point)))@i'
10. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let x = middle(a;b;c) in ax=bx ∧ ax=cx@i'
11. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point| 
                                                                                            aq=ay
                                                                                            ∧ (¬(q = p ∈ Point))} ].
      let uv = intersect pq (at radius xy) with Oab  in
          afst(uv)=ab
          ∧ asnd(uv)=ab
          ∧ p_fst(uv)_q
          ∧ snd(uv)_p_q
          ∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point)@i'
12. ∀[a,b,c:Point].  c-b-a supposing a-b-c@i'
13. ∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d)@i'
14. a : Point@i
15. b : Point@i
16. p : Point@i
17. q : {q:Point| ¬(q = p ∈ Point)} @i
18. x : {x:Point| a_x_b ∧ (¬(x = b ∈ Point))} @i
19. y : {y:Point| a_b_y} @i
20. ap=ax@i
21. aq=ay@i
⊢ afst(intersect pq (at radius xy) with Oab )=ab
∧ asnd(intersect pq (at radius xy) with Oab )=ab
∧ snd(intersect pq (at radius xy) with Oab )_p_q
∧ p_fst(intersect pq (at radius xy) with Oab )_q
∧ (¬((fst(intersect pq (at radius xy) with Oab )) = (snd(intersect pq (at radius xy) with Oab )) ∈ Point))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,p:Point.  \mforall{}q:\{q:Point|  \mneg{}(q  =  p)\}  .
    ((\mexists{}x:\{x:Point|  a\_x\_b  \mwedge{}  (\mneg{}(x  =  b))\}  .  \mexists{}y:\{y:Point|  a\_b\_y\}  .  (ap=ax  \mwedge{}  aq=ay))
    {}\mRightarrow{}  (\mexists{}y,z:Point.  (ay=ab  \mwedge{}  az=ab  \mwedge{}  z\_p\_q  \mwedge{}  p\_y\_q  \mwedge{}  (\mneg{}(y  =  z)))))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}fst(intersect  pq  (at  radius  xy)  with  Oab  )\mkleeneclose{}; 
              \mkleeneopen{}snd(intersect  pq  (at  radius  xy)  with  Oab  )\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  D  1
  THEN  (Unhide  THENA  Auto)
  THEN  D  2
  THEN  ExRepD)

---

Home Index