let a, b, r be real number ; :: 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) \ {s,t} c= inside_of_circle a,b,r
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) \ {s,t} c= inside_of_circle a,b,r )
assume A1: ( s in circle a,b,r & t in circle a,b,r ) ; :: thesis: (LSeg s,t) \ {s,t} c= inside_of_circle a,b,r
reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:13;
Sphere G,r = circle a,b,r by Th49;
then A2: Sphere |[a,b]|,r = circle a,b,r by Th15;
Ball |[a,b]|,r = inside_of_circle a,b,r by Th50;
hence (LSeg s,t) \ {s,t} c= inside_of_circle a,b,r by A1, A2, Th34; :: thesis: verum