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
(LSeg (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 (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} )
reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8;
Sphere (G,r) = circle (a,b,r) by Th47;
then A1: Sphere (|[a,b]|,r) = circle (a,b,r) by Th13;
assume ( s in circle (a,b,r) & t in circle (a,b,r) ) ; :: thesis: (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t}
hence (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} by A1, Th33; :: thesis: verum