let a, b, r be Real; :: thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds
(halfline (s,t)) /\ (circle (a,b,r)) = {s,t}
let s, t be Point of (TOP-REAL 2); :: thesis: ( s in circle (a,b,r) & t in circle (a,b,r) implies (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} )
assume A1: ( s in circle (a,b,r) & t in circle (a,b,r) ) ; :: thesis: (halfline (s,t)) /\ (circle (a,b,r)) = {s,t}
reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
circle (a,b,r) = Sphere (e,r) by Th47
.= Sphere (|[a,b]|,r) by Th13 ;
hence (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} by A1, Th34; :: thesis: verum